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:
set G = SymGroup X;
set H = SymGroup Y;
set h = SymGroupsIso p;
A2: dom p = X by FUNCT_2:def 1;
thus rng () c= the carrier of () ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of () c= rng ()
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of () or y in rng () )
assume y in the carrier of () ; :: thesis: y in rng ()
then reconsider y = y as Element of () ;
reconsider g = y as Permutation of Y by Th5;
A3: rng p = Y by ;
then reconsider p1 = p " as Function of Y,X by ;
A4: id Y = p * p1 by ;
A5: dom () = the carrier of () by FUNCT_2:def 1;
set x = (p1 * g) * p;
A6: rng p1 = X by ;
rng g = Y by FUNCT_2:def 3;
then rng (p1 * g) = X by ;
then rng ((p1 * g) * p) = X by ;
then (p1 * g) * p is Permutation of X by ;
then (p1 * g) * p in permutations X ;
then reconsider x = (p1 * g) * p as Element of () by Def2;
() . x = (p * x) * p1 by
.= ((p * (p1 * g)) * p) * p1 by RELAT_1:36
.= (p * (p1 * g)) * (p * p1) by RELAT_1:36
.= ((id Y) * g) * (id Y) by
.= g * (id Y) by FUNCT_2:17
.= y by FUNCT_2:17 ;
hence y in rng () by ; :: thesis: verum