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