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))}) )

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

hence
product J1 is SubSpace of product J2
by Th51; :: thesis: verum
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)) )

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 ) )

end;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

hence
[#] (product J1) in K1
by WAYBEL18:def 2; :: thesis: K1 = INTERSECTION (K2,{([#] (product J1))})
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;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

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

hence
K1 = INTERSECTION (K2,{([#] (product J1))})
by SETFAM_1:def 5; :: thesis: verum
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)

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

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)) )

end;( 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

thus
( U in K1 implies ex A, P0 being set st
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

end;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

hence
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
by A5, FUNCT_1:2; :: thesis: verum
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;

end;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 )
;

end;

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;.= (((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

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;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

( 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

given A, P0 being set such that A18:
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 )
; :: thesis: U in K1
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;( 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

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

hence
U in K1
by A25, WAYBEL18:def 2; :: thesis: verum
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;( 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