let I, J, K be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( f is_continuous_on [:[:I,J:],K:] & f = g implies for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )
assume that
A1: f is_continuous_on [:[:I,J:],K:] and
A2: f = g ; :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
set E = [:[:I,J:],K:];
A3: f is_uniformly_continuous_on [:[:I,J:],K:] by A1, Th2, NFCONT_2:10;
let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
then consider r being Real such that
A4: ( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st [x1,y1,z1] in [:[:I,J:],K:] & [x2,y2,z2] in [:[:I,J:],K:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) by A2, A3, Th3;
A5: for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e

proof

let x1, x2, y1, y2, z1, z2 be Real; :: thesis: ( x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r implies |.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e )
assume that
A6: ( x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K ) and
A7: ( |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r ) ; :: thesis: |.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e
( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] ) by A6, ZFMISC_1:87;
then ( [x1,y1,z1] in [:[:I,J:],K:] & [x2,y2,z2] in [:[:I,J:],K:] ) by A6, ZFMISC_1:87;
hence |.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e by A4, A7; :: thesis: verum

end;

take r ; :: thesis: ( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
thus ( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) by A4, A5; :: thesis: verum