let I be non empty set ; :: thesis: 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; :: thesis: 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)); :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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) ) )

A4: now :: thesis: for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open

let A be Subset of (product (Carrier J)); :: thesis: ( A in X implies (proj (J,(f /. A))) .: A is open )
assume A5: A in X ; :: thesis: (proj (J,(f /. A))) .: A is open
( A is empty implies (proj (J,(f /. A))) .: A = {} (J . (f /. A)) ) ;
hence (proj (J,(f /. A))) .: A is open by A2, A5, Th58; :: thesis: verum

end;

f " is non-empty

proof

assume not f " is non-empty ; :: thesis: contradiction
then {} in rng (f ") by RELAT_1:def 9;
then {} in X by A2, FUNCT_1:33;
then ( not X is empty & meet X = {} ) by SETFAM_1:4;
hence contradiction by A2, SETFAM_1:def 9; :: thesis: verum

end;

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; :: thesis: verum