let I be non empty set ; :: thesis: for J1, J2 being non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) holds
product J1 is SubSpace of product J2
let J1, J2 be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) implies product J1 is SubSpace of product J2 )
assume A1: for i being Element of I holds J1 . i is SubSpace of J2 . i ; :: thesis: product J1 is SubSpace of product J2
ex K1 being prebasis of (product J1) ex K2 being prebasis of (product J2) st
( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )

proof

reconsider K1 = product_prebasis J1 as prebasis of (product J1) by WAYBEL18:def 3;
reconsider K2 = product_prebasis J2 as prebasis of (product J2) by WAYBEL18:def 3;
take K1 ; :: thesis: ex K2 being prebasis of (product J2) st
( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )
take K2 ; :: thesis: ( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )
A2: [#] (product J1) = the carrier of (product J1) by STRUCT_0:def 3
.= product (Carrier J1) by WAYBEL18:def 3 ;
then [#] (product J1) = [#] (product (Carrier J1)) by SUBSET_1:def 3;
then reconsider P = [#] (product J1) as Subset of (product (Carrier J1)) ;
ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J1 . i & P = product ((Carrier J1) +* (i,V)) )

proof

set i = the Element of I;
take the Element of I ; :: thesis: ex T being TopStruct ex V being Subset of T st
( the Element of I in I & V is open & T = J1 . the Element of I & P = product ((Carrier J1) +* ( the Element of I,V)) )
take J1 . the Element of I ; :: thesis: ex V being Subset of (J1 . the Element of I) st
( the Element of I in I & V is open & J1 . the Element of I = J1 . the Element of I & P = product ((Carrier J1) +* ( the Element of I,V)) )
take [#] (J1 . the Element of I) ; :: thesis: ( the Element of I in I & [#] (J1 . the Element of I) is open & J1 . the Element of I = J1 . the Element of I & P = product ((Carrier J1) +* ( the Element of I,([#] (J1 . the Element of I)))) )
thus ( the Element of I in I & [#] (J1 . the Element of I) is open & J1 . the Element of I = J1 . the Element of I ) ; :: thesis: P = product ((Carrier J1) +* ( the Element of I,([#] (J1 . the Element of I))))
thus P = product ((Carrier J1) +* ( the Element of I,((Carrier J1) . the Element of I))) by A2, FUNCT_7:35
.= product ((Carrier J1) +* ( the Element of I,([#] (J1 . the Element of I)))) by PENCIL_3:7 ; :: thesis: verum

end;

hence [#] (product J1) in K1 by WAYBEL18:def 2; :: thesis: K1 = INTERSECTION (K2,{([#] (product J1))})
for U being set holds
( U in K1 iff ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) )

proof

let U be set ; :: thesis: ( U in K1 iff ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) )
A3: for i being Element of I
for V being Subset of (J1 . i)
for W being Subset of (J2 . i) st V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)

proof

let i be Element of I; :: thesis: for V being Subset of (J1 . i)
for W being Subset of (J2 . i) st V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
let V be Subset of (J1 . i); :: thesis: for W being Subset of (J2 . i) st V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
let W be Subset of (J2 . i); :: thesis: ( V = W /\ ([#] (J1 . i)) implies (Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1) )
assume A4: V = W /\ ([#] (J1 . i)) ; :: thesis: (Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
A5: dom ((Carrier J1) +* (i,V)) = I by PARTFUN1:def 2
.= dom (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) by PARTFUN1:def 2 ;
for x being object st x in dom ((Carrier J1) +* (i,V)) holds
((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x

proof

let x be object ; :: thesis: ( x in dom ((Carrier J1) +* (i,V)) implies ((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x )
assume a6: x in dom ((Carrier J1) +* (i,V)) ; :: thesis: ((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x
then A6: x in dom (Carrier J1) by FUNCT_7:30;
A7: x in I by a6;
reconsider j = x as Element of I by a6;
A8: x in dom (Carrier J2) by A7, PARTFUN1:def 2;

per cases ( x = i or x <> i ) ;

suppose A9: x = i ; :: thesis: ((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x

hence ((Carrier J1) +* (i,V)) . x = V by A6, FUNCT_7:31
.= (((Carrier J2) +* (i,W)) . x) /\ ([#] (J1 . i)) by A4, A8, A9, FUNCT_7:31
.= (((Carrier J2) +* (i,W)) . x) /\ ((Carrier J1) . i) by PENCIL_3:7
.= (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x by A9, PBOOLE:def 5 ;
:: thesis: verum

end;

suppose A10: x <> i ; :: thesis: ((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x

A11: ( (Carrier J1) . j = [#] (J1 . j) & (Carrier J2) . j = [#] (J2 . j) ) by PENCIL_3:7;
a12: J1 . j is SubSpace of J2 . j by A1;
thus ((Carrier J1) +* (i,V)) . x = (Carrier J1) . x by A10, FUNCT_7:32
.= ((Carrier J2) . x) /\ ((Carrier J1) . x) by a12, XBOOLE_1:28, A11, PRE_TOPC:def 4
.= (((Carrier J2) +* (i,W)) . x) /\ ((Carrier J1) . x) by A10, FUNCT_7:32
.= (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x by a6, PBOOLE:def 5 ; :: thesis: verum

end;

end;

end;

hence (Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1) by A5, FUNCT_1:2; :: thesis: verum

end;

thus ( U in K1 implies ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) ) :: thesis: ( ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) implies U in K1 )

proof

assume U in K1 ; :: thesis: ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 )
then consider i being set , T being TopStruct , V being Subset of T such that
A13: ( i in I & V is open & T = J1 . i ) and
A14: U = product ((Carrier J1) +* (i,V)) by WAYBEL18:def 2;
reconsider i = i as Element of I by A13;
A15: V in the topology of (J1 . i) by A13, PRE_TOPC:def 2;
reconsider V = V as Subset of (J1 . i) by A13;
J1 . i is SubSpace of J2 . i by A1;
then consider W being Subset of (J2 . i) such that
A16: ( W in the topology of (J2 . i) & V = W /\ ([#] (J1 . i)) ) by A15, PRE_TOPC:def 4;
set A = product ((Carrier J2) +* (i,W));
take product ((Carrier J2) +* (i,W)) ; :: thesis: ex P0 being set st
( product ((Carrier J2) +* (i,W)) in K2 & P0 in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P0 )
take P ; :: thesis: ( product ((Carrier J2) +* (i,W)) in K2 & P in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P )
(Carrier J2) . i = [#] (J2 . i) by PENCIL_3:7
.= the carrier of (J2 . i) by STRUCT_0:def 3 ;
then ( i in dom (Carrier J2) & W c= (Carrier J2) . i ) by A13, PARTFUN1:def 2;
then A17: product ((Carrier J2) +* (i,W)) is Subset of (product (Carrier J2)) by Th39;
ex i9 being set ex T9 being TopStruct ex V9 being Subset of T9 st
( i9 in I & V9 is open & T9 = J2 . i9 & product ((Carrier J2) +* (i,W)) = product ((Carrier J2) +* (i9,V9)) ) by A16, PRE_TOPC:def 2;
hence product ((Carrier J2) +* (i,W)) in K2 by A17, WAYBEL18:def 2; :: thesis: ( P in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P )
thus P in {([#] (product J1))} by TARSKI:def 1; :: thesis: U = (product ((Carrier J2) +* (i,W))) /\ P
thus U = product (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) by A14, A16, A3
.= (product ((Carrier J2) +* (i,W))) /\ P by A2, Th33 ; :: thesis: verum

end;

given A, P0 being set such that A18: ( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) ; :: thesis: U in K1
consider i being set , T being TopStruct , W being Subset of T such that
A19: ( i in I & W is open & T = J2 . i ) and
A20: A = product ((Carrier J2) +* (i,W)) by A18, WAYBEL18:def 2;
reconsider i = i as Element of I by A19;
A21: W in the topology of (J2 . i) by A19, PRE_TOPC:def 2;
reconsider W = W as Subset of (J2 . i) by A19;
set V = W /\ ([#] (J1 . i));
A22: W /\ ([#] (J1 . i)) c= [#] (J1 . i) by XBOOLE_1:17;
reconsider V = W /\ ([#] (J1 . i)) as Subset of (J1 . i) ;
P0 = product (Carrier J1) by A2, A18, TARSKI:def 1;
then A23: U = product (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) by A18, A20, Th33
.= product ((Carrier J1) +* (i,V)) by A3 ;
A24: i in dom (Carrier J1) by A19, PARTFUN1:def 2;
V c= (Carrier J1) . i by A22, PENCIL_3:7;
then A25: U c= product (Carrier J1) by A23, A24, Th39;
ex i9 being set ex T9 being TopStruct ex V9 being Subset of T9 st
( i9 in I & V9 is open & T9 = J1 . i9 & U = product ((Carrier J1) +* (i9,V9)) )

proof

take i ; :: thesis: ex T9 being TopStruct ex V9 being Subset of T9 st
( i in I & V9 is open & T9 = J1 . i & U = product ((Carrier J1) +* (i,V9)) )
take J1 . i ; :: thesis: ex V9 being Subset of (J1 . i) st
( i in I & V9 is open & J1 . i = J1 . i & U = product ((Carrier J1) +* (i,V9)) )
take V ; :: thesis: ( i in I & V is open & J1 . i = J1 . i & U = product ((Carrier J1) +* (i,V)) )
thus i in I ; :: thesis: ( V is open & J1 . i = J1 . i & U = product ((Carrier J1) +* (i,V)) )
J1 . i is SubSpace of J2 . i by A1;
then V in the topology of (J1 . i) by A21, PRE_TOPC:def 4;
hence ( V is open & J1 . i = J1 . i & U = product ((Carrier J1) +* (i,V)) ) by A23, PRE_TOPC:def 2; :: thesis: verum

end;

hence U in K1 by A25, WAYBEL18:def 2; :: thesis: verum

end;

hence K1 = INTERSECTION (K2,{([#] (product J1))}) by SETFAM_1:def 5; :: thesis: verum

end;

hence product J1 is SubSpace of product J2 by Th51; :: thesis: verum