let X, Y be non empty set ; :: thesis: for p being Function of X,Y st p is bijective holds

SymGroupsIso p is onto

let p be Function of X,Y; :: thesis: ( p is bijective implies SymGroupsIso p is onto )

assume A1: p is bijective ; :: thesis: 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) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (SymGroup Y) c= rng (SymGroupsIso p)

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (SymGroup Y) or y in rng (SymGroupsIso p) )

assume y in the carrier of (SymGroup Y) ; :: thesis: 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; :: thesis: verum

SymGroupsIso p is onto

let p be Function of X,Y; :: thesis: ( p is bijective implies SymGroupsIso p is onto )

assume A1: p is bijective ; :: thesis: 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) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (SymGroup Y) c= rng (SymGroupsIso p)

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (SymGroup Y) or y in rng (SymGroupsIso p) )

assume y in the carrier of (SymGroup Y) ; :: thesis: 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; :: thesis: verum