defpred S₁[ set ] means verum;
let I be non empty set ; :: thesis:
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: 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:
deffunc H₁( set ) -> Element of bool the carrier of (product J) = (proj (J,i)) " $1;
defpred S₂[ object , object ] means ex A being set st
( A = $2 & $1 in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = $2 holds
V is open ) );
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:
A4: for xi being object st xi in the carrier of (J . i) holds
ex Ai being object st
( Ai in bool the carrier of (J . i) & S₂[xi,Ai] )

let xi be object ; :: thesis:
assume xi in the carrier of (J . i) ; :: thesis:
then reconsider xi9 = xi as Element of (J . i) ;
consider G being finite Subset of F such that
A5: (proj (J,i)) " {xi9} 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, Th21;
take Ai ; :: thesis:
thus Ai in bool the carrier of (J . i) ; :: thesis:
take Ai ; :: thesis:
thus Ai = Ai ; :: 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 object st xi in the carrier of (J . i) holds
S₂[xi,h . xi] from FUNCT_1:sch 6(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 object ; :: according to TARSKI:def 3 :: thesis:
assume A13: x in [#] (J . i) ; :: thesis:
then S₂[x,h . x] by A11;
then consider A being set such that
A14: ( A = h . x & x in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = h . x holds
V is open ) ) ;
( x in h . x & h . x in bGip ) by A9, FUNCT_1:def 3, A14, A13;
hence x in union bGip by 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 object such that
A15: ( x in dom h & P = h . x ) by FUNCT_1:def 3;
S₂[x,h . x] by A9, A11, A15;
hence P is open by A15; :: thesis:

end;

then A16: 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
A17: Gip c= bGip and
A18: [#] (J . i) c= union Gip and
A19: Gip is finite by A12, A16, Th14;
reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by A18, A19, ZFMISC_1:2;
set Gp = { H₁(Ai) where Ai is Element of Gip : S₁[Ai] } ;
A20: { H₁(Ai) where Ai is Element of Gip : S₁[Ai] } c= F

let A be object ; :: 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
A21: A = (proj (J,i)) " Ai ;
Ai in Gip ;
then consider x being object such that
A22: ( x in dom h & h . x = Ai ) by A17, FUNCT_1:def 3;
S₂[x,h . x] by A9, A11, A22;
hence A in F by A21, A22; :: thesis:

end;

{ H₁(Ai) where Ai is Element of Gip : S₁[Ai] } is finite from PRE_CIRC:sch 1();
then reconsider Gp = { H₁(Ai) where Ai is Element of Gip : S₁[Ai] } as finite Subset of F by A20;
[#] (product J) c= union Gp by A18, Th18;
hence contradiction by A2; :: thesis: