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 ) )
reconsider f1 = ||.f.|| as PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real ;
||.f.|| = |.g.| by A2, Th9;
hence 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 ) ) by A1, Th8, MESFUN16:22; :: thesis: verum