let I be 2 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I

for i, j being Element of I

for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I

for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let i, j be Element of I; :: thesis: for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let P be Subset of (product (Carrier J)); :: thesis: ( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

assume A1: ( i <> j & P in product_prebasis J ) ; :: thesis: ( ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then consider k being set , T being TopStruct , U being Subset of T such that

A2: ( k in I & U is open & T = J . k & P = product ((Carrier J) +* (k,U)) ) by WAYBEL18:def 2;

k in {i,j} by A1, A2, Th8;

for i, j being Element of I

for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I

for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let i, j be Element of I; :: thesis: for P being Subset of (product (Carrier J)) holds

( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

let P be Subset of (product (Carrier J)); :: thesis: ( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

assume A1: ( i <> j & P in product_prebasis J ) ; :: thesis: ( ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then consider k being set , T being TopStruct , U being Subset of T such that

A2: ( k in I & U is open & T = J . k & P = product ((Carrier J) +* (k,U)) ) by WAYBEL18:def 2;

k in {i,j} by A1, A2, Th8;

per cases then
( k = i or k = j )
by TARSKI:def 2;

end;

suppose A3:
k = i
; :: thesis: ( ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then reconsider V = U as Subset of (J . i) by A2;

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum

end;now :: thesis: ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) )

hence
( ex V being Subset of (J . i) st ( V is open & P = product ((i,j) --> (V,([#] (J . j)))) )

take V = V; :: thesis: ( V is open & P = product ((i,j) --> (V,([#] (J . j)))) )

thus V is open by A2, A3; :: thesis: P = product ((i,j) --> (V,([#] (J . j))))

(Carrier J) . j = [#] (J . j) by PENCIL_3:7;

hence P = product ((i,j) --> (V,([#] (J . j)))) by A2, A1, A3, Th34; :: thesis: verum

end;thus V is open by A2, A3; :: thesis: P = product ((i,j) --> (V,([#] (J . j))))

(Carrier J) . j = [#] (J . j) by PENCIL_3:7;

hence P = product ((i,j) --> (V,([#] (J . j)))) by A2, A1, A3, Th34; :: thesis: verum

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum

suppose A4:
k = j
; :: thesis: ( ex V being Subset of (J . i) st

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then reconsider W = U as Subset of (J . j) by A2;

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum

end;now :: thesis: ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )

hence
( ex V being Subset of (J . i) st ( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )

take W = W; :: thesis: ( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )

thus W is open by A2, A4; :: thesis: P = product ((i,j) --> (([#] (J . i)),W))

(Carrier J) . i = [#] (J . i) by PENCIL_3:7;

hence P = product ((i,j) --> (([#] (J . i)),W)) by A2, A1, A4, Th34; :: thesis: verum

end;thus W is open by A2, A4; :: thesis: P = product ((i,j) --> (([#] (J . i)),W))

(Carrier J) . i = [#] (J . i) by PENCIL_3:7;

hence P = product ((i,j) --> (([#] (J . i)),W)) by A2, A1, A4, Th34; :: thesis: verum

( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st

( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum