let n be non zero Nat; :: thesis: for D being n -element FinSequence
for J being closed_interval Subset of REAL
for E being Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & E = [:(CarProduct D),J:] holds
E is compact
let D be n -element FinSequence; :: thesis: for J being closed_interval Subset of REAL
for E being Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & E = [:(CarProduct D),J:] holds
E is compact
let J be closed_interval Subset of REAL; :: thesis: for E being Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & E = [:(CarProduct D),J:] holds
E is compact
let E be Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:]; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & E = [:(CarProduct D),J:] implies E is compact )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: E = [:(CarProduct D),J:] ; :: thesis: E is compact
A3: ( not D is non-empty implies CarProduct D = {} ) by Th6;

now :: thesis: ( D is non-empty implies E is compact )

assume D is non-empty ; :: thesis: E is compact
then consider I being Subset of (CarProduct ((Seg n) --> RNS_Real)) such that
A4: ( I = CarProduct D & I is compact ) by A1, MEASUR15:51;
reconsider J1 = J as Subset of RNS_Real ;
J1 is compact by MESFUN16:7;
hence E is compact by A2, A4, MESFUN16:8; :: thesis: verum

end;

hence E is compact by A2, A3; :: thesis: verum