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= rng (SymGroupsIso p)
let y be object ; TARSKI:def 3 ( not y in the carrier of (SymGroup Y) or y in rng (SymGroupsIso p) )
assume
y in the carrier of (SymGroup Y)
; y in rng (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:25;
A4:
id Y = p * p1
by A1, A3, FUNCT_2:29;
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:33;
rng g = Y
by FUNCT_2:def 3;
then
rng (p1 * g) = X
by A6, FUNCT_2:14;
then
rng ((p1 * g) * p) = X
by A3, FUNCT_2:14;
then
(p1 * g) * p is Permutation of X
by A1, FUNCT_2:57;
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:36
.=
(p * (p1 * g)) * (p * p1)
by RELAT_1:36
.=
((id Y) * g) * (id Y)
by A4, RELAT_1:36
.=
g * (id Y)
by FUNCT_2:17
.=
y
by FUNCT_2:17
;
hence
y in rng (SymGroupsIso p)
by A5, FUNCT_1:def 3; verum