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

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

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 )

given V being Subset of (J . i) such that A6:
( V is open & P = product ({i} --> V) )
; :: thesis: P in product_prebasis J( 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;( 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

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