let X, Y be non empty set ; for p being Function of X,Y st p is bijective holds
SymGroupsIso p is onto
let p be Function of X,Y; ( p is bijective implies SymGroupsIso p is onto )
assume A1:
p is bijective
; SymGroupsIso p is onto
set G = SymGroup X;
set H = SymGroup Y;
set h = SymGroupsIso p;
A2:
dom p = X
by FUNCT_2:def 1;
thus
rng (SymGroupsIso p) c= the carrier of (SymGroup Y)
; XBOOLE_0:def 10,FUNCT_2:def 3 the carrier of (SymGroup Y) c= proj2 (SymGroupsIso p)
let y be set ; TARSKI:def 3 ( not y in the carrier of (SymGroup Y) or y in proj2 (SymGroupsIso p) )
assume
y in the carrier of (SymGroup Y)
; y in proj2 (SymGroupsIso p)
then reconsider y = y as Element of (SymGroup Y) ;
reconsider g = y as Permutation of Y by Th5;
A3:
rng p = Y
by A1, FUNCT_2:def 3;
then reconsider p1 = p " as Function of Y,X by A1, FUNCT_2:31;
A4:
id Y = p * p1
by A1, A3, FUNCT_2:35;
A5:
dom (SymGroupsIso p) = the carrier of (SymGroup X)
by FUNCT_2:def 1;
set x = (p1 * g) * p;
A6:
rng p1 = X
by A1, A2, FUNCT_1:55;
rng g = Y
by FUNCT_2:def 3;
then
rng (p1 * g) = X
by A6, FUNCT_2:20;
then
rng ((p1 * g) * p) = X
by A3, FUNCT_2:20;
then
(p1 * g) * p is Permutation of X
by A1, FUNCT_2:83;
then
(p1 * g) * p in permutations X
;
then reconsider x = (p1 * g) * p as Element of (SymGroup X) by Def2;
(SymGroupsIso p) . x =
(p * x) * p1
by A1, Def3
.=
((p * (p1 * g)) * p) * p1
by RELAT_1:55
.=
(p * (p1 * g)) * (p * p1)
by RELAT_1:55
.=
((id Y) * g) * (id Y)
by A4, RELAT_1:55
.=
g * (id Y)
by FUNCT_2:23
.=
y
by FUNCT_2:23
;
hence
y in proj2 (SymGroupsIso p)
by A5, FUNCT_1:def 5; verum