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 ()) 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 ()) 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 ()) 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 ()); :: 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:
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)) ) )
;
suppose ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) ; :: thesis:
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 (() +* (i,V)) by A1, A2, Th34;
hence P in product_prebasis J by ; :: thesis: verum
end;
suppose ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ; :: thesis:
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 (() +* (j,W)) by A1, A3, Th34;
hence P in product_prebasis J by ; :: thesis: verum
end;
end;