let I be non empty set ; :: thesis:
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis:
let i be Element of I; :: thesis:
let F be Subset of (product_prebasis J); :: thesis:
assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis:
let xi be Element of (J . i); :: thesis:
let G be finite Subset of F; :: thesis:
assume (proj J,i) " {xi} c= union G ; :: thesis:
then consider A being set such that
A2: A in product_prebasis J and
A3: A in G and
A4: (proj J,i) " {xi} c= A by A1, Th21;
A <> [#] (product J)

assume A5: A = [#] (product J) ; :: thesis:
reconsider G1 = {A} as finite Subset of F by A3, ZFMISC_1:37;
union G1 = [#] (product J) by A5, ZFMISC_1:31;
hence contradiction by A1; :: thesis:

end;

then consider Ai being Subset of (J . i) such that
A6: Ai <> [#] (J . i) and
A7: xi in Ai and
A8: Ai is open and
A9: A = (proj J,i) " Ai by A2, A4, Th18;
take Ai ; :: thesis:
thus Ai <> [#] (J . i) by A6; :: thesis:
thus xi in Ai by A7; :: thesis:
thus (proj J,i) " Ai in G by A3, A9; :: thesis:
thus Ai is open by A8; :: thesis: