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]

proof

let x be object ; :: thesis: ( x in I1 implies ex y being object st S₁[x,y] )
assume x in I1 ; :: thesis: ex y being object st S₁[x,y]
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: S₁[x,f]
take i ; :: thesis: ex f being Function of (J1 . i),((J2 * p) . i) st
( x = i & f = f & f is being_homeomorphism )
take f ; :: thesis: ( x = i & f = f & f is being_homeomorphism )
thus ( x = i & f = f & f is being_homeomorphism ) by A4; :: thesis: verum

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 )

proof

let i be Element of I1; :: thesis: ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism )
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: ( F . i = f & f is being_homeomorphism )
thus ( F . i = f & f is being_homeomorphism ) by A7; :: thesis: verum

end;

for x being object st x in dom F holds
F . x is Function

proof

let x be object ; :: thesis: ( x in dom F implies F . x is Function )
assume x in dom F ; :: thesis: F . x is Function
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: verum

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] )

proof

let x be object ; :: thesis: ( x in the carrier of (product J1) implies ex y being object st
( y in the carrier of (product J2) & S₂[x,y] ) )
assume x in the carrier of (product J1) ; :: thesis: ex y being object st
( y in the carrier of (product J2) & S₂[x,y] )
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: ( h in the carrier of (product J2) & S₂[x,h] )
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

proof

let x be object ; :: thesis: ( x in dom (Carrier J2) implies h . x in (Carrier J2) . x )
assume x in dom (Carrier J2) ; :: thesis: h . x in (Carrier J2) . x
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: verum

end;

then H: h in product (Carrier J2) by A11, CARD_3:9;
hence h in the carrier of (product J2) by WAYBEL18:def 3; :: thesis: S₂[x,h]
reconsider h = h as Element of (product J2) by H, WAYBEL18:def 3;
take g ; :: thesis: ex h being Element of (product J2) st
( x = g & h = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g . i) ) )
take h ; :: thesis: ( x = g & h = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g . i) ) )

now :: thesis: for i being Element of I1 holds h . (p . i) = (F . i) . (g . i)

let i be Element of I1; :: thesis: h . (p . i) = (F . i) . (g . i)
i in I1 ;
then A17: i in dom p by PARTFUN1:def 2;
then p9 . i in rng p9 by FUNCT_1:3;
then A18: p9 . i in dom (p9 ") by FUNCT_1:33;
thus h . (p . i) = h0 . ((p9 ") . (p9 . i)) by A18, FUNCT_1:13
.= h0 . i by A17, FUNCT_1:34
.= (F . i) . (g . i) by A10 ; :: thesis: verum

end;

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

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: ex F being ManySortedFunction of I1 st
( ( 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) ) )
take F ; :: thesis: ( ( 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) ) )

now :: thesis: for g being Element of (product J1)
for i being Element of I1 holds (IT . g) . (p . i) = (F . i) . (g . i)

let g be Element of (product J1); :: thesis: for i being Element of I1 holds (IT . g) . (p . i) = (F . i) . (g . i)
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: (IT . g) . (p . i) = (F . i) . (g . i)
thus (IT . g) . (p . i) = (F . i) . (g . i) by A20; :: thesis: verum

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: verum