let n be non zero Nat; :: thesis: for D being n -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let D be n -element FinSequence; :: thesis: for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] implies for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: f = g and
A3: f is_continuous_on [:(CarProduct D),J:] ; :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A4: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact )

proof

now :: thesis: ( not D is non-empty implies ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact ) )

assume not D is non-empty ; :: thesis: ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact )
then A5: CarProduct D = {} by Th6;
reconsider I = CarProduct D as Subset of (CarProduct ((Seg n) --> RNS_Real)) by A4, MEASUR15:42;
I is compact by A5;
hence ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact ) ; :: thesis: verum

end;

hence ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact ) by A1, MEASUR15:51; :: thesis: verum

end;

then consider I being Subset of (CarProduct ((Seg n) --> RNS_Real)) such that
A6: ( I = CarProduct D & I is compact ) ;
reconsider J1 = J as Subset of RNS_Real ;
A7: J1 is compact by MESFUN16:7;
reconsider E = [:(CarProduct D),J1:] as Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] by A6, A7, MESFUN16:8;
E is compact by A1, Th35;
then f is_uniformly_continuous_on [:(CarProduct D),J:] by A3, NFCONT_2:10;
hence for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) by A2, Th36; :: thesis: verum