A3:
dom p = X
by A1, FUNCT_2:def 1;

A4: rng p = Y by A2, FUNCT_2:def 3;

reconsider p1 = p " as Function of Y,X by A2, A4, FUNCT_2:25;

A5: rng p1 = X by A2, A3, FUNCT_1:33;

defpred S_{1}[ Function, set ] means $2 = (p * $1) * p1;

A6: for x being Element of (SymGroup X) ex y being Element of (SymGroup Y) st S_{1}[x,y]

for x being Element of (SymGroup X) holds S_{1}[x,h . x]
from FUNCT_2:sch 3(A6);

hence ex b_{1} being Function of (SymGroup X),(SymGroup Y) st

for x being Element of (SymGroup X) holds b_{1} . x = (p * x) * (p ")
; :: thesis: verum

A4: rng p = Y by A2, FUNCT_2:def 3;

reconsider p1 = p " as Function of Y,X by A2, A4, FUNCT_2:25;

A5: rng p1 = X by A2, A3, FUNCT_1:33;

defpred S

A6: for x being Element of (SymGroup X) ex y being Element of (SymGroup Y) st S

proof

ex h being Function of (SymGroup X),(SymGroup Y) st
let x be Element of (SymGroup X); :: thesis: ex y being Element of (SymGroup Y) st S_{1}[x,y]

reconsider f = x as Permutation of X by Th5;

set y = (p * f) * p1;

rng f = X by FUNCT_2:def 3;

then rng (p * f) = Y by A4, A1, FUNCT_2:14;

then rng ((p * f) * p1) = Y by A1, A5, FUNCT_2:14;

then (p * f) * p1 is Permutation of Y by A2, A1, FUNCT_2:57;

then (p * f) * p1 in permutations Y ;

then reconsider y = (p * f) * p1 as Element of (SymGroup Y) by Def2;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;reconsider f = x as Permutation of X by Th5;

set y = (p * f) * p1;

rng f = X by FUNCT_2:def 3;

then rng (p * f) = Y by A4, A1, FUNCT_2:14;

then rng ((p * f) * p1) = Y by A1, A5, FUNCT_2:14;

then (p * f) * p1 is Permutation of Y by A2, A1, FUNCT_2:57;

then (p * f) * p1 in permutations Y ;

then reconsider y = (p * f) * p1 as Element of (SymGroup Y) by Def2;

take y ; :: thesis: S

thus S

for x being Element of (SymGroup X) holds S

hence ex b

for x being Element of (SymGroup X) holds b