let X, Y be set ; ( X,Y are_equipotent implies SymGroup X, SymGroup Y are_isomorphic )
assume A1:
X,Y are_equipotent
; 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 A5:
X <> {}
;
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
;
GROUP_6:def 11 h is bijective thus
(
h is
one-to-one &
h is
onto )
by A2, A5, A6, A7, Th11, Th12;
FUNCT_2:def 4 verum end;