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

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

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

f " is non-empty
(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;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

proof

hence
for i being Element of I holds
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;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

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