let I1, I2 be non empty set ; :: thesis: for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; :: thesis: for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; :: thesis: for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let p be Function of I1,I2; :: thesis: for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let H be ProductHomeo of J1,J2,p; :: thesis: for F being ManySortedFunction of I1 st p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let F be ManySortedFunction of I1; :: thesis: ( p is bijective & ( 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 (H . g) . (p . i) = (F . i) . (g . i) ) implies for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) )

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: for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))

let i be Element of I1; :: thesis: for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let U be Subset of (J1 . i); :: thesis: H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
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
.= [#] (J2 . j) by
.= 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: ( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )
thus ( y in H .: (product ((Carrier J1) +* (i,U))) implies y in product ((Carrier J2) +* (j,((F . i) .: U))) ) :: thesis: ( y in product ((Carrier J2) +* (j,((F . i) .: U))) implies y in H .: (product ((Carrier J1) +* (i,U))) )
proof
assume y in H .: (product ((Carrier J1) +* (i,U))) ; :: thesis: y in product ((Carrier J2) +* (j,((F . i) .: U)))
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 ;
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: ( z in dom ((Carrier J2) +* (j,((F . i) .: U))) implies h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z )
assume a11: z in dom ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
then A11: z in dom (Carrier J2) by FUNCT_7:30;
reconsider j0 = z as Element of I2 by a11;
I2 = rng p by ;
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 ( j0 = j or j0 <> j ) ;
suppose A15: j0 = j ; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
then A16: ((Carrier J2) +* (j,((F . i) .: U))) . z = (F . i) .: U by ;
A17: i0 = i by ;
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 ;
then g . i in U by ;
hence h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z by ; :: thesis: verum
end;
suppose j0 <> j ; :: thesis: h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
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 ; :: thesis: verum
end;
end;
end;
hence y in product ((Carrier J2) +* (j,((F . i) .: U))) by ; :: thesis: verum
end;
assume A20: y in product ((Carrier J2) +* (j,((F . i) .: U))) ; :: thesis: y in H .: (product ((Carrier J1) +* (i,U)))
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 ;
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 ;
then A25: ( j in dom (Carrier J2) & (F . i) .: U c= (Carrier J2) . j ) by ;
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 S1[ 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 S1[i0,y]
proof
let i0 be Element of I1; :: thesis: ex y being object st S1[i0,y]
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: S1[i0,(f0 ") . (h . (p . i0))]
take f0 ; :: thesis: ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) )
thus ( F . i0 = f0 & (f0 ") . (h . (p . i0)) = (f0 ") . (h . (p . i0)) ) by A29; :: thesis: verum
end;
consider g being ManySortedSet of I1 such that
A30: for i being Element of I1 holds S1[i,g . i] from take g ; :: thesis: ( g in dom H & g in product ((Carrier J1) +* (i,U)) & H . g = y )
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: ( z in dom ((Carrier J1) +* (i,U)) implies g . z in ((Carrier J1) +* (i,U)) . z )
assume z in dom ((Carrier J1) +* (i,U)) ; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z
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 ;
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 ( i = i0 or i <> i0 ) ;
suppose A35: i = i0 ; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z
then A36: ((Carrier J1) +* (i,U)) . z = U by ;
j in dom ((Carrier J2) +* (j,((F . i) .: U))) by ;
then h . j in ((Carrier J2) +* (j,((F . i) .: U))) . j by ;
then A37: h . j in (F . i) .: U by ;
A38: f " = f0 " by ;
[#] ((J2 * p) . i0) = rng f by
.= dom (f0 ") by ;
then g . i0 in rng (f0 ") by ;
then A39: g . i0 in dom f by ;
h . j in (Carrier J2) . j by ;
then h . j in [#] (J2 . j) by PENCIL_3:7;
then a40: h . j in [#] ((J2 * p) . i) by ;
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 ;
f . ((f ") . (h . j)) = f1 . ((f1 ") . (h . j)) by
.= h . j by ;
then g . i0 in f0 " (f0 .: U) by ;
hence g . z in ((Carrier J1) +* (i,U)) . z by ; :: thesis: verum
end;
suppose i <> i0 ; :: thesis: g . z in ((Carrier J1) +* (i,U)) . z
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
.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;
then (f0 ") . (h . (p . i0)) in rng (f0 ") by ;
then g . i0 in dom f0 by ;
then g . i0 in [#] (J1 . i0) by ;
hence g . z in ((Carrier J1) +* (i,U)) . z by ; :: thesis: verum
end;
end;
end;
then g in product ((Carrier J1) +* (i,U)) by ;
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 ; :: thesis: H . g = y
reconsider h0 = H . g as Element of (product J2) by ;
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 ;
for z being object st z in dom h holds
h . z = h0 . z
proof
let z be object ; :: thesis: ( z in dom h implies h . z = h0 . z )
assume z in dom h ; :: thesis: h . z = h0 . z
then z in dom (Carrier J2) by ;
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 ;
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
.= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3 ;
A54: p . i0 = j0 by ;
A55: (Carrier J2) . (p . i0) = [#] (J2 . (p . i0)) by PENCIL_3:7
.= [#] ((J2 * p) . i0) by
.= 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 ;
h . j0 = f9 . ((f9 ") . (h . (p . i0))) by
.= h0 . j0 by A3, A47, A51, A54 ;
hence h . z = h0 . z ; :: thesis: verum
end;
hence H . g = y by ; :: thesis: verum
end;
hence y in H .: (product ((Carrier J1) +* (i,U))) by FUNCT_1:def 6; :: thesis: verum
end;
hence H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) by TARSKI:2; :: thesis: verum