let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds
product J is compact
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is compact ) implies product J is compact )
assume A1: for i being Element of I holds J . i is compact ; :: thesis: product J is compact
reconsider B = product_prebasis J as prebasis of (product J) by WAYBEL18:def 3;
assume not product J is compact ; :: thesis: contradiction
then consider F being Subset of B such that
A2: [#] (product J) c= union F and
A3: for G being finite Subset of F holds not [#] (product J) c= union G by Th15;
defpred S₁[ set , Element of I] means for G being finite Subset of F holds not (proj (J,$2)) " {$1} c= union G;
A4: for i being Element of I ex xi being Element of (J . i) st S₁[xi,i] by A1, A3, Th22;
consider f being Element of (product J) such that
A5: for i being Element of I holds S₁[f . i,i] from YELLOW17:sch 1(A4);
f in [#] (product J) ;
then consider A being set such that
A6: f in A and
A7: A in F by A2, TARSKI:def 4;
reconsider G = {A} as finite Subset of F by A7, ZFMISC_1:31;
consider i being Element of I, Ai being Subset of (J . i) such that
Ai is open and
A8: (proj (J,i)) " Ai = A by A7, Th16;
(proj (J,i)) . f in Ai by A6, A8, FUNCT_1:def 7;
then f . i in Ai by Th8;
then {(f . i)} c= Ai by ZFMISC_1:31;
then (proj (J,i)) " {(f . i)} c= A by A8, RELAT_1:143;
then (proj (J,i)) " {(f . i)} c= union G by ZFMISC_1:25;
hence contradiction by A5; :: thesis: verum