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₁[ Function, set ] means $2 = (p * $1) * p1;
A6: for x being Element of (SymGroup X) ex y being Element of (SymGroup Y) st S₁[x,y]

proof

let x be Element of (SymGroup X); :: thesis: ex y being Element of (SymGroup Y) st S₁[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₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

ex h being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds S₁[x,h . x] from FUNCT_2:sch 3(A6);
hence ex b₁ being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b₁ . x = (p * x) * (p ") ; :: thesis: verum