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;

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 <> {} )
;

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;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