let I be 1 -element set ; 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; 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; 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)); ( 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)
; 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;
suppose A6:
rng f = {i}
;
ex V being Subset of (J . i) st
( 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
;
( V is open & P = product ({i} --> V) )
(
V0 is
empty or not
V0 is
empty )
;
hence
V is
open
by A3, A9, Th58;
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;
verum end; end;