let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of st ( for i being Element of I holds J . i is compact ) holds
product J is compact
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: 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 Th16;
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, Th23;
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;
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, Th17;
reconsider G = {A} as finite Subset of F by A7, ZFMISC_1:37;
(proj J,i) . f in Ai by A6, A8, FUNCT_1:def 13;
then f . i in Ai by Th8;
then {(f . i)} c= Ai by ZFMISC_1:37;
then (proj J,i) " {(f . i)} c= A by A8, RELAT_1:178;
then (proj J,i) " {(f . i)} c= union G by ZFMISC_1:31;
hence contradiction by A5; :: thesis: verum