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 that
A1: for i being Element of I holds J . i is compact and
A2: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis:
assume A3: for xi being Element of (J . i) ex G being finite Subset of F st (proj J,i) " {xi} c= union G ; :: thesis:
defpred S₁[ set , set ] means ( $1 in $2 & (proj J,i) " $2 in F & ( for V being Subset of (J . i) st V = $2 holds
V is open ) );
A4: for xi being set st xi in the carrier of (J . i) holds
ex Ai being set st
( Ai in bool the carrier of (J . i) & S₁[xi,Ai] )

let xi be set ; :: thesis:
assume xi in the carrier of (J . i) ; :: thesis:
then reconsider xi' = xi as Element of (J . i) ;
consider G being finite Subset of F such that
A5: (proj J,i) " {xi'} c= union G by A3;
consider Ai being Subset of (J . i) such that
Ai <> [#] (J . i) and
A6: xi in Ai and
A7: (proj J,i) " Ai in G and
A8: Ai is open by A2, A5, Th22;
take Ai ; :: thesis:
thus Ai in bool the carrier of (J . i) ; :: thesis:
thus xi in Ai by A6; :: thesis:
thus (proj J,i) " Ai in F by A7; :: thesis:
let V be Subset of (J . i); :: thesis:
assume V = Ai ; :: thesis:
hence V is open by A8; :: thesis:

end;

consider h being Function such that
A9: dom h = the carrier of (J . i) and
A10: rng h c= bool the carrier of (J . i) and
A11: for xi being set st xi in the carrier of (J . i) holds
S₁[xi,h . xi] from WELLORD2:sch 1(A4);
reconsider bGip = rng h as Subset-Family of (J . i) by A10;
reconsider bGip = bGip as Subset-Family of (J . i) ;
A12: [#] (J . i) c= union bGip

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A13: x in [#] (J . i) ; :: thesis:
then A14: x in h . x by A11;
h . x in bGip by A9, A13, FUNCT_1:def 5;
hence x in union bGip by A14, TARSKI:def 4; :: thesis:

end;

for P being Subset of (J . i) st P in bGip holds
P is open

let P be Subset of (J . i); :: thesis:
assume P in bGip ; :: thesis:
then consider x being set such that
A15: x in dom h and
A16: P = h . x by FUNCT_1:def 5;
thus P is open by A9, A11, A15, A16; :: thesis:

end;

then A17: bGip is open by TOPS_2:def 1;
J . i is compact by A1;
then consider Gip being Subset-Family of (J . i) such that
A18: Gip c= bGip and
A19: [#] (J . i) c= union Gip and
A20: Gip is finite by A12, A17, Th15;
reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by A19, A20, ZFMISC_1:2;
deffunc H₁( set ) -> Element of bool the carrier of (product J) = (proj J,i) " $1;
defpred S₂[ set ] means verum;
set Gp = { H₁(Ai) where Ai is Element of Gip : S₂[Ai] } ;
A21: { H₁(Ai) where Ai is Element of Gip : S₂[Ai] } is finite from PRE_CIRC:sch 1();
{ H₁(Ai) where Ai is Element of Gip : S₂[Ai] } c= F

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in { H₁(Ai) where Ai is Element of Gip : S₂[Ai] } ; :: thesis:
then consider Ai being Element of Gip such that
A22: A = (proj J,i) " Ai ;
Ai in Gip ;
then consider x being set such that
A23: x in dom h and
A24: h . x = Ai by A18, FUNCT_1:def 5;
thus A in F by A9, A11, A22, A23, A24; :: thesis:

end;

then reconsider Gp = { H₁(Ai) where Ai is Element of Gip : S₂[Ai] } as finite Subset of F by A21;
[#] (product J) c= union Gp by A19, Th19;
hence contradiction by A2; :: thesis: