let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product J) holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of (product J) holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let i be Element of I; :: thesis: for P being Subset of (product J) holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let P be Subset of (product J); :: thesis: ( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

hereby :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) implies P is open )

assume P is open ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )
then P in the topology of (product J) by PRE_TOPC:def 2;
then P in product_prebasis J by Th65;
hence ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) by Th64; :: thesis: verum

end;

A1: P is Subset of (product (Carrier J)) by WAYBEL18:def 3;
assume ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) ; :: thesis: P is open
then P in product_prebasis J by A1, Th64;
then P in the topology of (product J) by Th65;
hence P is open by PRE_TOPC:def 2; :: thesis: verum