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 I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 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 I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 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 I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) )

assume P in FinMeetCl (product_prebasis J) ; :: thesis: ex I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

then consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that

A1: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and

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) ) ) by Th62;

reconsider I0 = rng f as finite Subset of I by A1, FINSET_1:8;

take I0 ; :: thesis: for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

thus for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) by A2; :: thesis: verum

for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds

ex I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 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 I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 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 I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) )

assume P in FinMeetCl (product_prebasis J) ; :: thesis: ex I0 being finite Subset of I st

for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

then consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that

A1: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and

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) ) ) by Th62;

reconsider I0 = rng f as finite Subset of I by A1, FINSET_1:8;

take I0 ; :: thesis: for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

thus for i being Element of I holds

( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) by A2; :: thesis: verum