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

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

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

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;

end;