let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let i be Element of I; :: thesis: for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let F be Subset of (product_prebasis J); :: thesis: ( ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )

assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis: for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let xi be Element of (J . i); :: thesis: for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let G be finite Subset of F; :: thesis: ( (proj (J,i)) " {xi} c= union G implies ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )

assume (proj (J,i)) " {xi} c= union G ; :: thesis: ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

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, Th20;

A <> [#] (product J)

A5: Ai <> [#] (J . i) and

A6: xi in Ai and

A7: Ai is open and

A8: A = (proj (J,i)) " Ai by A2, A4, Th17;

take Ai ; :: thesis: ( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

thus Ai <> [#] (J . i) by A5; :: thesis: ( xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

thus xi in Ai by A6; :: thesis: ( (proj (J,i)) " Ai in G & Ai is open )

thus (proj (J,i)) " Ai in G by A3, A8; :: thesis: Ai is open

thus Ai is open by A7; :: thesis: verum

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let i be Element of I; :: thesis: for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let F be Subset of (product_prebasis J); :: thesis: ( ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )

assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis: for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let xi be Element of (J . i); :: thesis: for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

let G be finite Subset of F; :: thesis: ( (proj (J,i)) " {xi} c= union G implies ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )

assume (proj (J,i)) " {xi} c= union G ; :: thesis: ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

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, Th20;

A <> [#] (product J)

proof

then consider Ai being Subset of (J . i) such that
reconsider G1 = {A} as finite Subset of F by A3, ZFMISC_1:31;

assume A = [#] (product J) ; :: thesis: contradiction

then union G1 = [#] (product J) by ZFMISC_1:25;

hence contradiction by A1; :: thesis: verum

end;assume A = [#] (product J) ; :: thesis: contradiction

then union G1 = [#] (product J) by ZFMISC_1:25;

hence contradiction by A1; :: thesis: verum

A5: Ai <> [#] (J . i) and

A6: xi in Ai and

A7: Ai is open and

A8: A = (proj (J,i)) " Ai by A2, A4, Th17;

take Ai ; :: thesis: ( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

thus Ai <> [#] (J . i) by A5; :: thesis: ( xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

thus xi in Ai by A6; :: thesis: ( (proj (J,i)) " Ai in G & Ai is open )

thus (proj (J,i)) " Ai in G by A3, A8; :: thesis: Ai is open

thus Ai is open by A7; :: thesis: verum