let I be non empty set ; for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
let P be non empty Subset of (product (Carrier J)); ( P in FinMeetCl (product_prebasis J) implies ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) ) )
assume A1:
P in FinMeetCl (product_prebasis J)
; ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that
A2:
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X )
and
A3:
P = product ((Carrier J) +* (product_basis_selector (J,f)))
by A1, Lm3;
take
X
; ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
take
f
; ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
thus
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X )
by A2; for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) )
f " is non-empty
hence
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) )
by A2, A3, A4, Th60; verum