let I1, I2 be non empty set ; :: thesis:
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis:
let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis:
let p be Function of I1,I2; :: thesis:
let H be ProductHomeo of J1,J2,p; :: thesis:
let F be ManySortedFunction of I1; :: thesis:
assume that
A1: p is bijective and
A2: for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) and
A3: for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ; :: thesis:
let i be Element of I1; :: thesis:
let U be Subset of (J1 . i); :: thesis:
reconsider j = p . i as Element of I2 ;
i in I1 ;
then A4: i in dom p by FUNCT_2:def 1;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A5: ( F . i = f & f is being_homeomorphism ) by A2;
A6: rng f = [#] ((J2 * p) . i) by A5, TOPS_2:def 5
.= [#] (J2 . j) by A4, FUNCT_1:13
.= the carrier of (J2 . j) by STRUCT_0:def 3 ;
for y being object holds
( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )

proof

let y be object ; :: thesis:
thus ( y in H .: (product ((Carrier J1) +* (i,U))) implies y in product ((Carrier J2) +* (j,((F . i) .: U))) ) :: thesis:

proof

assume y in H .: (product ((Carrier J1) +* (i,U))) ; :: thesis:
then consider x being object such that
A8: ( x in dom H & x in product ((Carrier J1) +* (i,U)) & y = H . x ) by FUNCT_1:def 6;
reconsider g = x as Element of (product J1) by A8;
y in rng H by A8, FUNCT_1:3;
then reconsider h = y as Element of (product J2) ;
h in the carrier of (product J2) ;
then A9: h in product (Carrier J2) by WAYBEL18:def 3;
then A10: dom h = dom (Carrier J2) by CARD_3:9
.= dom ((Carrier J2) +* (j,((F . i) .: U))) by FUNCT_7:30 ;
for z being object st z in dom ((Carrier J2) +* (j,((F . i) .: U))) holds
h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z

proof

let z be object ; :: thesis:
assume a11: z in dom ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis:
then A11: z in dom (Carrier J2) by FUNCT_7:30;
reconsider j0 = z as Element of I2 by a11;
I2 = rng p by A1, FUNCT_2:def 3;
then consider i0 being object such that
A12: ( i0 in I1 & p . i0 = j0 ) by FUNCT_2:11;
reconsider i0 = i0 as Element of I1 by A12;
consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that
A13: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;
A14: h . j0 = f0 . (g . i0) by A3, A8, A12, A13;

per cases ;

suppose A15: j0 = j ; :: thesis:

then A16: ((Carrier J2) +* (j,((F . i) .: U))) . z = (F . i) .: U by A11, FUNCT_7:31;
A17: i0 = i by A1, A12, A15, FUNCT_2:19;
a18: I1 = dom (Carrier J1) by PARTFUN1:def 2;
then i in dom (Carrier J1) ;
then i in dom ((Carrier J1) +* (i,U)) by FUNCT_7:30;
then g . i in ((Carrier J1) +* (i,U)) . i by A8, CARD_3:9;
then g . i in U by a18, FUNCT_7:31;
hence h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z by A14, A16, A17, A13, FUNCT_2:35; :: thesis:

end;

suppose j0 <> j ; :: thesis:

then ((Carrier J2) +* (j,((F . i) .: U))) . z = (Carrier J2) . z by FUNCT_7:32;
hence h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z by A9, A11, CARD_3:9; :: thesis:

end;

hence y in product ((Carrier J2) +* (j,((F . i) .: U))) by A10, CARD_3:9; :: thesis:

end;

assume A20: y in product ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis:
then reconsider h = y as Element of product ((Carrier J2) +* (j,((F . i) .: U))) ;
A21: the carrier of (J1 . i) = [#] (J1 . i) by STRUCT_0:def 3
.= (Carrier J1) . i by PENCIL_3:7 ;
i in I1 ;
then A22: i in dom (Carrier J1) by PARTFUN1:def 2;
then A23: product ((Carrier J1) +* (i,U)) c= product (Carrier J1) by A21, Th39;
A24: (Carrier J2) . j = [#] (J2 . j) by PENCIL_3:7
.= the carrier of (J2 . j) by STRUCT_0:def 3 ;
a25: ( j in I2 & (F . i) .: U c= the carrier of (J2 . j) ) by A6, A5, RELAT_1:111;
then A25: ( j in dom (Carrier J2) & (F . i) .: U c= (Carrier J2) . j ) by A24, PARTFUN1:def 2;
then A26: product ((Carrier J2) +* (j,((F . i) .: U))) c= product (Carrier J2) by Th39;
ex x being object st
( x in dom H & x in product ((Carrier J1) +* (i,U)) & H . x = y )

proof

defpred S₁[ object , object ] means ex f being one-to-one Function st
( F . $1 = f & $2 = (f ") . (h . (p . $1)) );
A28: for i0 being Element of I1 ex y being object st S₁[i0,y]

proof

let i0 be Element of I1; :: thesis:
consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that
A29: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;
reconsider f0 = f0 as one-to-one Function by A29;
take (f0 ") . (h . (p . i0)) ; :: thesis:
take f0 ; :: thesis:
thus ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) ) by A29; :: thesis:

end;

consider g being ManySortedSet of I1 such that
A30: for i being Element of I1 holds S₁[i,g . i] from PBOOLE:sch 6(A28);
take g ; :: thesis:
A31: dom g = I1 by PARTFUN1:def 2
.= dom ((Carrier J1) +* (i,U)) by PARTFUN1:def 2 ;
a36: for z being object st z in dom ((Carrier J1) +* (i,U)) holds
g . z in ((Carrier J1) +* (i,U)) . z

proof

let z be object ; :: thesis:
assume z in dom ((Carrier J1) +* (i,U)) ; :: thesis:
then reconsider i0 = z as Element of I1 ;
consider f0 being one-to-one Function such that
A32: ( F . i0 = f0 & g . i0 = (f0 ") . (h . (p . i0)) ) by A30;
p . i0 in I2 ;
then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;
then h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;
then h . (p . i0) in [#] (J2 . (p . i0)) by PENCIL_3:7;
then A33: h . (p . i0) in [#] ((J2 * p) . i0) by FUNCT_2:15;

per cases ;

suppose A35: i = i0 ; :: thesis:

then A36: ((Carrier J1) +* (i,U)) . z = U by A22, FUNCT_7:31;
j in dom ((Carrier J2) +* (j,((F . i) .: U))) by a25, PARTFUN1:def 2;
then h . j in ((Carrier J2) +* (j,((F . i) .: U))) . j by A20, CARD_3:9;
then A37: h . j in (F . i) .: U by A25, FUNCT_7:31;
A38: f " = f0 " by A5, A32, A35, TOPS_2:def 4;
[#] ((J2 * p) . i0) = rng f by A5, A35, TOPS_2:def 5
.= dom (f0 ") by A5, A32, A35, FUNCT_1:33 ;
then g . i0 in rng (f0 ") by A32, A33, FUNCT_1:3;
then A39: g . i0 in dom f by A5, A32, A35, FUNCT_1:33;
h . j in (Carrier J2) . j by A20, A26, A25, CARD_3:9;
then h . j in [#] (J2 . j) by PENCIL_3:7;
then a40: h . j in [#] ((J2 * p) . i) by A4, FUNCT_1:13;
a41: dom f = the carrier of (J1 . i) by FUNCT_2:def 1;
reconsider f1 = f as one-to-one Function by A5;
A43: h . j in rng f1 by a40, A5, TOPS_2:def 5;
f . ((f ") . (h . j)) = f1 . ((f1 ") . (h . j)) by A5, TOPS_2:def 4
.= h . j by A43, FUNCT_1:35 ;
then g . i0 in f0 " (f0 .: U) by A5, A32, A35, A38, A39, A37, FUNCT_1:def 7;
hence g . z in ((Carrier J1) +* (i,U)) . z by A36, a41, A5, A32, A35, FUNCT_1:94; :: thesis:

end;

suppose i <> i0 ; :: thesis:

then A44: ((Carrier J1) +* (i,U)) . z = (Carrier J1) . z by FUNCT_7:32;
consider f9 being Function of (J1 . i0),((J2 * p) . i0) such that
A45: ( F . i0 = f9 & f9 is being_homeomorphism ) by A2;
dom (f0 ") = rng f0 by FUNCT_1:33
.= [#] ((J2 * p) . i0) by A32, A45, TOPS_2:def 5
.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;
then (f0 ") . (h . (p . i0)) in rng (f0 ") by A33, FUNCT_1:3;
then g . i0 in dom f0 by A32, FUNCT_1:33;
then g . i0 in [#] (J1 . i0) by A32, A45, TOPS_2:def 5;
hence g . z in ((Carrier J1) +* (i,U)) . z by A44, PENCIL_3:7; :: thesis:

end;

then g in product ((Carrier J1) +* (i,U)) by A31, CARD_3:9;
then g in product (Carrier J1) by A23;
then A47: g in the carrier of (product J1) by WAYBEL18:def 3;
hence ( g in dom H & g in product ((Carrier J1) +* (i,U)) ) by a36, A31, CARD_3:9, FUNCT_2:def 1; :: thesis:
reconsider h0 = H . g as Element of (product J2) by A47, FUNCT_2:5;
h0 in the carrier of (product J2) ;
then h0 in product (Carrier J2) by WAYBEL18:def 3;
then A48: dom h0 = dom (Carrier J2) by CARD_3:9
.= dom h by A20, A26, CARD_3:9 ;
for z being object st z in dom h holds
h . z = h0 . z

proof

let z be object ; :: thesis:
assume z in dom h ; :: thesis:
then z in dom (Carrier J2) by A20, A26, CARD_3:9;
then reconsider j0 = z as Element of I2 ;
reconsider p9 = p as one-to-one Function by A1;
j0 in I2 ;
then A49: j0 in rng p9 by A1, FUNCT_2:def 3;
then j0 in dom (p9 ") by FUNCT_1:33;
then (p9 ") . j0 in rng (p9 ") by FUNCT_1:3;
then A50: (p9 ") . j0 in dom p9 by FUNCT_1:33;
then reconsider i0 = (p9 ") . j0 as Element of I1 by FUNCT_2:def 1;
consider f9 being one-to-one Function such that
A51: ( F . i0 = f9 & g . i0 = (f9 ") . (h . (p . i0)) ) by A30;
consider f0 being Function of (J1 . i0),((J2 * p) . i0) such that
A52: ( F . i0 = f0 & f0 is being_homeomorphism ) by A2;
A53: rng f9 = [#] ((J2 * p) . i0) by A51, A52, TOPS_2:def 5
.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;
A54: p . i0 = j0 by A49, FUNCT_1:35;
A55: (Carrier J2) . (p . i0) = [#] (J2 . (p . i0)) by PENCIL_3:7
.= [#] ((J2 * p) . i0) by A50, FUNCT_1:13
.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;
p . i0 in I2 ;
then p . i0 in dom (Carrier J2) by PARTFUN1:def 2;
then A56: h . (p . i0) in (Carrier J2) . (p . i0) by A20, A26, CARD_3:9;
h . j0 = f9 . ((f9 ") . (h . (p . i0))) by A53, A54, A55, A56, FUNCT_1:35
.= h0 . j0 by A3, A47, A51, A54 ;
hence h . z = h0 . z ; :: thesis:

end;

hence H . g = y by A48, FUNCT_1:2; :: thesis:

end;

hence y in H .: (product ((Carrier J1) +* (i,U))) by FUNCT_1:def 6; :: thesis:

end;

hence H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) by TARSKI:2; :: thesis: