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 (Carrier J)) 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 (Carrier J)) 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 (Carrier J)) 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
.= (Carrier J) . i by PENCIL_3:7 ;
then A2: Carrier J = {i} --> the carrier of (J . i) by A1, Th7;
let P be Subset of (product (Carrier J)); :: 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 ((Carrier J) +* (j,V)) by WAYBEL18:def 2;
A5: i = j by A1, A3, TARSKI:def 1;
reconsider W = V as Subset of (J . i) by A1, A3, TARSKI:def 1;
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 A2, A4, A5, FUNCOP_1:def 9
.= 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 in product_prebasis J
P = product (i .--> V) by A6, FUNCOP_1:def 9
.= product ((i .--> the carrier of (J . i)) +* (i,V)) by Th44
.= product ((Carrier J) +* (i,V)) by A2, FUNCOP_1:def 9 ;
hence P in product_prebasis J by A6, WAYBEL18:def 2; :: thesis: verum