defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in I1 implies ex y being object st S1[x,y] )
assume x in I1 ; :: thesis: ex y being object st S1[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 ;
take f ; :: thesis: S1[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
S1[x,F . x] from 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 S2[ 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) & S2[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) & S2[x,y] ) )

assume x in the carrier of (product J1) ; :: thesis: ex y being object st
( y in the carrier of (product J2) & S2[x,y] )

then reconsider g = x as Element of (product J1) ;
deffunc H1( object ) -> set = (F . \$1) . (g . \$1);
consider h0 being ManySortedSet of I1 such that
A10: for i being Element of I1 holds h0 . i = H1(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 ;
then reconsider h = h0 * (p9 ") as ManySortedSet of I2 by ;
take h ; :: thesis: ( h in the carrier of (product J2) & S2[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 ;
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 ;
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 ;
then h . j in [#] (J2 . j) by ;
hence h . x in (Carrier J2) . x by PENCIL_3:7; :: thesis: verum
end;
then H: h in product (Carrier J2) by ;
hence h in the carrier of (product J2) by WAYBEL18:def 3; :: thesis: S2[x,h]
reconsider h = h as Element of (product J2) by ;
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
.= h0 . i by
.= (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
S2[x,IT . x] from 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