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

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of (product ()) holds
( P in product_prebasis J 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 ()) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
the carrier of (J . i) = [#] (J . i) by STRUCT_0:def 3
.= () . i by PENCIL_3:7 ;
then A2: Carrier J = {i} --> the carrier of (J . i) by ;
let P be Subset of (product ()); :: thesis: ( P in product_prebasis J 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 in product_prebasis J )
assume P in product_prebasis J ; :: thesis: ex W being Subset of (J . i) st
( W is open & P = product ({i} --> W) )

then consider j being set , T being TopStruct , V being Subset of T such that
A3: ( j in I & V is open & T = J . j ) and
A4: P = product (() +* (j,V)) by WAYBEL18:def 2;
A5: i = j by ;
reconsider W = V as Subset of (J . i) by ;
take W = W; :: thesis: ( W is open & P = product ({i} --> W) )
thus W is open by A3, A5; :: thesis: P = product ({i} --> W)
thus P = product ((i .--> the carrier of (J . i)) +* (i,W)) by
.= product (i .--> W) by Th44
.= product ({i} --> W) by FUNCOP_1:def 9 ; :: thesis: verum
end;
given V being Subset of (J . i) such that A6: ( V is open & P = product ({i} --> V) ) ; :: thesis:
P = product (i .--> V) by
.= product ((i .--> the carrier of (J . i)) +* (i,V)) by Th44
.= product (() +* (i,V)) by ;
hence P in product_prebasis J by ; :: thesis: verum