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

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

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 )

A1:
P is Subset of (product (Carrier J))
by WAYBEL18:def 3;( 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;( 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

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