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:
reconsider B = product_prebasis J as prebasis of () by WAYBEL18:def 3;
assume not product J is compact ; :: thesis: contradiction
then consider F being Subset of B such that
A2: [#] () c= union F and
A3: for G being finite Subset of F holds not [#] () c= union G by Th15;
defpred S1[ 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 S1[xi,i] by A1, A3, Th22;
consider f being Element of () such that
A5: for i being Element of I holds S1[f . i,i] from f in [#] () ;
then consider A being set such that
A6: f in A and
A7: A in F by ;
reconsider G = {A} as finite Subset of F by ;
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 ;
(proj (J,i)) . f in Ai by ;
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 ;
then (proj (J,i)) " {(f . i)} c= union G by ZFMISC_1:25;
hence contradiction by A5; :: thesis: verum