defpred S₁[ object , object ] means ex i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( $1 = i & $2 = f & f is being_homeomorphism );
A3: for x being object st x in I1 holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in I1 ; :: thesis:
then reconsider i = x as Element of I1 ;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A4: f is being_homeomorphism by A2, T_0TOPSP:def 1;
take f ; :: thesis:
take i ; :: thesis:
take f ; :: thesis:
thus ( x = i & f = f & f is being_homeomorphism ) by A4; :: thesis:

end;

consider F being ManySortedSet of I1 such that
A5: for x being object st x in I1 holds
S₁[x,F . x] from PBOOLE:sch 3(A3);
A6: for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism )

let i be Element of I1; :: thesis:
consider j being Element of I1, f being Function of (J1 . j),((J2 * p) . j) such that
A7: ( i = j & F . i = f & f is being_homeomorphism ) by A5;
reconsider f = f as Function of (J1 . i),((J2 * p) . i) by A7;
take f ; :: thesis:
thus ( F . i = f & f is being_homeomorphism ) by A7; :: thesis:

end;

let x be object ; :: thesis:
assume x in dom F ; :: thesis:
then reconsider i = x as Element of I1 ;
ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) by A6;
hence F . x is Function ; :: thesis:

end;

then reconsider F = F as ManySortedFunction of I1 by FUNCOP_1:def 6;
defpred S₂[ object , object ] means ex g being Element of (product J1) ex h being Element of (product J2) st
( $1 = g & $2 = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g . i) ) );
A9: for x being object st x in the carrier of (product J1) holds
ex y being object st
( y in the carrier of (product J2) & S₂[x,y] )

let x be object ; :: thesis:
assume x in the carrier of (product J1) ; :: thesis:
then reconsider g = x as Element of (product J1) ;
deffunc H₁( object ) -> set = (F . $1) . (g . $1);
consider h0 being ManySortedSet of I1 such that
A10: for i being Element of I1 holds h0 . i = H₁(i) from PBOOLE:sch 5();
reconsider p9 = p as one-to-one Function by A1;
rng (p9 ") = dom p9 by FUNCT_1:33
.= I1 by FUNCT_2:def 1
.= dom h0 by PARTFUN1:def 2 ;
then dom (h0 * (p9 ")) = dom (p9 ") by RELAT_1:27
.= rng p9 by FUNCT_1:33
.= I2 by A1, FUNCT_2:def 3 ;
then reconsider h = h0 * (p9 ") as ManySortedSet of I2 by PARTFUN1:def 2, RELAT_1:def 18;
take h ; :: thesis:
A11: dom h = I2 by PARTFUN1:def 2
.= dom (Carrier J2) by PARTFUN1:def 2 ;
for x being object st x in dom (Carrier J2) holds
h . x in (Carrier J2) . x

let x be object ; :: thesis:
assume x in dom (Carrier J2) ; :: thesis:
then reconsider j = x as Element of I2 ;
j in I2 ;
then A12: j in rng p9 by A1, FUNCT_2:def 3;
then A13: j in dom (p9 ") by FUNCT_1:33;
then (p9 ") . j in rng (p9 ") by FUNCT_1:3;
then (p9 ") . j in dom p9 by FUNCT_1:33;
then reconsider i = (p9 ") . j as Element of I1 by FUNCT_2:def 1;
A14: (F . i) . (g . i) = h0 . i by A10
.= h . j by A13, FUNCT_1:13 ;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A15: ( F . i = f & f is being_homeomorphism ) by A6;
A16: f . (g . i) in the carrier of ((J2 * p) . i) ;
i in I1 ;
then i in dom p by FUNCT_2:def 1;
then (J2 * p) . i = J2 . (p . i) by FUNCT_1:13
.= J2 . j by A12, FUNCT_1:35 ;
then h . j in [#] (J2 . j) by A14, A15, A16, STRUCT_0:def 3;
hence h . x in (Carrier J2) . x by PENCIL_3:7; :: thesis:

end;

end;

hence ( x = g & h = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g . i) ) ) ; :: thesis:

end;

consider IT being Function of the carrier of (product J1), the carrier of (product J2) such that
A19: for x being object st x in the carrier of (product J1) holds
S₂[x,IT . x] from FUNCT_2:sch 1(A9);
reconsider IT = IT as Function of (product J1),(product J2) ;
take IT ; :: thesis:
take F ; :: thesis:

let g be Element of (product J1); :: thesis:
A20: ex g0 being Element of (product J1) ex h being Element of (product J2) st
( g = g0 & IT . g = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g0 . i) ) ) by A19;
let i be Element of I1; :: thesis:
thus (IT . g) . (p . i) = (F . i) . (g . i) by A20; :: thesis:

end;

hence ( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (IT . g) . (p . i) = (F . i) . (g . i) ) ) by A6; :: thesis: