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 (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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 (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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)) st P in FinMeetCl (product_prebasis J) holds

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 FinMeetCl (product_prebasis J) implies ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) ) )

assume P in FinMeetCl (product_prebasis J) ; :: thesis: ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) )

then consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that

A3: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and

A4: P = product ((Carrier J) +* (product_basis_selector (J,f))) by Lm3;

set F = (Carrier J) +* (product_basis_selector (J,f));

for i being Element of I

for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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 (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

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)) st P in FinMeetCl (product_prebasis J) holds

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 FinMeetCl (product_prebasis J) implies ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) ) )

assume P in FinMeetCl (product_prebasis J) ; :: thesis: ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) )

then consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that

A3: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and

A4: P = product ((Carrier J) +* (product_basis_selector (J,f))) by Lm3;

set F = (Carrier J) +* (product_basis_selector (J,f));

per cases
( rng f = {} or rng f = {i} )
by A1, ZFMISC_1:33;

end;

suppose
rng f = {}
; :: thesis: ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) )

( V is open & P = product ({i} --> V) )

then a5:
product_basis_selector (J,f) = {}
;

take [#] (J . i) ; :: thesis: ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) )

thus ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) ) by a5, A2, A4, STRUCT_0:def 3; :: thesis: verum

end;take [#] (J . i) ; :: thesis: ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) )

thus ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) ) by a5, A2, A4, STRUCT_0:def 3; :: thesis: verum

suppose A6:
rng f = {i}
; :: thesis: ex V being Subset of (J . i) st

( V is open & P = product ({i} --> V) )

( V is open & P = product ({i} --> V) )

then A7:
dom f = {((f ") . i)}
by Th1;

A8: i in rng f by A6, TARSKI:def 1;

A9: (f ") . i in X by A3, A7, TARSKI:def 1;

then reconsider V0 = (f ") . i as Subset of (product (Carrier J)) ;

reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;

take V ; :: thesis: ( V is open & P = product ({i} --> V) )

( V0 is empty or not V0 is empty ) ;

hence V is open by A3, A9, Th58; :: thesis: P = product ({i} --> V)

A10: product_basis_selector (J,f) = {i} --> ((product_basis_selector (J,f)) . i) by A6, Th7

.= {i} --> ((proj (J,i)) .: V0) by A8, Th54 ;

dom (Carrier J) = {i} by A1, PARTFUN1:def 2;

then dom (Carrier J) = dom (product_basis_selector (J,f)) by A6, PARTFUN1:def 2;

hence P = product ({i} --> V) by A4, A10, FUNCT_4:19; :: thesis: verum

end;A8: i in rng f by A6, TARSKI:def 1;

A9: (f ") . i in X by A3, A7, TARSKI:def 1;

then reconsider V0 = (f ") . i as Subset of (product (Carrier J)) ;

reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;

take V ; :: thesis: ( V is open & P = product ({i} --> V) )

( V0 is empty or not V0 is empty ) ;

hence V is open by A3, A9, Th58; :: thesis: P = product ({i} --> V)

A10: product_basis_selector (J,f) = {i} --> ((product_basis_selector (J,f)) . i) by A6, Th7

.= {i} --> ((proj (J,i)) .: V0) by A8, Th54 ;

dom (Carrier J) = {i} by A1, PARTFUN1:def 2;

then dom (Carrier J) = dom (product_basis_selector (J,f)) by A6, PARTFUN1:def 2;

hence P = product ({i} --> V) by A4, A10, FUNCT_4:19; :: thesis: verum