defpred S_{1}[ 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_{1}[x,y]

A5: for x being object st x in I1 holds

S_{1}[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 )

F . x is Function

defpred S_{2}[ 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_{2}[x,y] )

A19: for x being object st x in the carrier of (product J1) holds

S_{2}[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) ) )

( 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

( $1 = i & $2 = f & f is being_homeomorphism );

A3: for x being object st x in I1 holds

ex y being object st S

proof

consider F being ManySortedSet of I1 such that
let x be object ; :: thesis: ( x in I1 implies ex y being object st S_{1}[x,y] )

assume x in I1 ; :: thesis: ex y being object st S_{1}[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_{1}[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;assume x in I1 ; :: thesis: ex y being object st S

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

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

A5: for x being object st x in I1 holds

S

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

for x being object st x in dom F holds
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;( 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

F . x is Function

proof

then reconsider F = F as ManySortedFunction of I1 by FUNCOP_1:def 6;
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;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

defpred S

( $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

proof

consider IT being Function of the carrier of (product J1), the carrier of (product J2) such that
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_{2}[x,y] ) )

assume x in the carrier of (product J1) ; :: thesis: ex y being object st

( y in the carrier of (product J2) & S_{2}[x,y] )

then reconsider g = x as Element of (product J1) ;

deffunc H_{1}( 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_{1}(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_{2}[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

hence h in the carrier of (product J2) by WAYBEL18:def 3; :: thesis: S_{2}[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) ) )

end;( y in the carrier of (product J2) & S

assume x in the carrier of (product J1) ; :: thesis: ex y being object st

( y in the carrier of (product J2) & S

then reconsider g = x as Element of (product J1) ;

deffunc H

consider h0 being ManySortedSet of I1 such that

A10: for i being Element of I1 holds h0 . i = H

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

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

then H:
h in product (Carrier J2)
by A11, CARD_3:9;
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;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

hence h in the carrier of (product J2) by WAYBEL18:def 3; :: thesis: S

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)

hence
( x = g & h = h & ( for i being Element of I1 holds h . (p . i) = (F . i) . (g . i) ) )
; :: thesis: verumlet 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;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

A19: for x being object st x in the carrier of (product J1) holds

S

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)

hence
( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st 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;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

( 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