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)) st i <> j holds

( P in product_prebasis J iff ( 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)) st i <> j holds

( P in product_prebasis J iff ( 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)) st i <> j holds

( P in product_prebasis J iff ( 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: ( i <> j implies ( P in product_prebasis J iff ( 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 ; :: thesis: ( P in product_prebasis J iff ( 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)) ) ) )

hence ( 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)) ) ) by Lm8; :: 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)) ) ) implies P in product_prebasis J )

assume ( 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)) ) ) ; :: thesis: P in product_prebasis J

for i, j being Element of I

for P being Subset of (product (Carrier J)) st i <> j holds

( P in product_prebasis J iff ( 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)) st i <> j holds

( P in product_prebasis J iff ( 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)) st i <> j holds

( P in product_prebasis J iff ( 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: ( i <> j implies ( P in product_prebasis J iff ( 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 ; :: thesis: ( P in product_prebasis J iff ( 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)) ) ) )

hence ( 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)) ) ) by Lm8; :: 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)) ) ) implies P in product_prebasis J )

assume ( 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)) ) ) ; :: thesis: P in product_prebasis J

per cases then
( 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)) ) ) ;

end;

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

suppose
ex V being Subset of (J . i) st

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

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

then consider V being Subset of (J . i) such that

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

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

then P = product ((Carrier J) +* (i,V)) by A1, A2, Th34;

hence P in product_prebasis J by A2, WAYBEL18:def 2; :: thesis: verum

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

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

then P = product ((Carrier J) +* (i,V)) by A1, A2, Th34;

hence P in product_prebasis J by A2, WAYBEL18:def 2; :: thesis: verum

suppose
ex W being Subset of (J . j) st

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

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

then consider W being Subset of (J . j) such that

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

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

then P = product ((Carrier J) +* (j,W)) by A1, A3, Th34;

hence P in product_prebasis J by A3, WAYBEL18:def 2; :: thesis: verum

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

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

then P = product ((Carrier J) +* (j,W)) by A1, A3, Th34;

hence P in product_prebasis J by A3, WAYBEL18:def 2; :: thesis: verum