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_{1}[ 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_{1}[xi,i]
by A1, A3, Th22;

consider f being Element of (product J) such that

A5: for i being Element of I holds S_{1}[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

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

A4: for i being Element of I ex xi being Element of (J . i) st S

consider f being Element of (product J) such that

A5: for i being Element of I holds S

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