A1: dom p = X by B1, FUNCT_2:def 1;
A2: rng p = Y by B2, FUNCT_2:def 3;
reconsider p1 = p " as Function of Y,X by B2, A2, FUNCT_2:25;
A3: rng p1 = X by B2, A1, FUNCT_1:33;
defpred S₁[ Function, set ] means $2 = (p * $1) * p1;
A4: 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 A2, B1, FUNCT_2:14;
then rng ((p * f) * p1) = Y by B1, A3, FUNCT_2:14;
then (p * f) * p1 is Permutation of Y by B2, B1, 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(A4);
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