let X, Y be set ; :: thesis: ( X,Y are_equipotent implies SymGroup X, SymGroup Y are_isomorphic )
assume A1: X,Y are_equipotent ; :: thesis: SymGroup X, SymGroup Y are_isomorphic
then consider p being Function such that
A2: p is one-to-one and
A3: dom p = X and
A4: rng p = Y by WELLORD2:def 4;

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: SymGroup X, SymGroup Y are_isomorphic

hence SymGroup X, SymGroup Y are_isomorphic by A1, CARD_1:26; :: thesis: verum

end;

suppose A5: X <> {} ; :: thesis: SymGroup X, SymGroup Y are_isomorphic

then A6: Y <> {} by A1, CARD_1:26;
reconsider p = p as Function of X,Y by A3, A4, FUNCT_2:2;
A7: p is onto by A4;
then reconsider h = SymGroupsIso p as Homomorphism of (SymGroup X),(SymGroup Y) by A2, A5, A6, Th10;
take h ; :: according to GROUP_6:def 11 :: thesis: h is bijective
thus ( h is one-to-one & h is onto ) by A2, A5, A6, A7, Th11, Th12; :: according to FUNCT_2:def 4 :: thesis: verum

end;

end;