let I be non empty set ; :: thesis:
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis:
let P be non empty Subset of (product (Carrier J)); :: thesis:
assume A1: P in FinMeetCl (product_prebasis J) ; :: thesis:
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:
take f ; :: thesis:
thus ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) by A2; :: thesis:

A4: now :: thesis:

let A be Subset of (product (Carrier J)); :: thesis:
assume A5: A in X ; :: thesis:
( 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:

end;

f " is non-empty

assume not f " is non-empty ; :: thesis:
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:

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: