let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & 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 u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )
let x, y be Element 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 [:[:I,J:],K:] = dom f & 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 u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < 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 [:[:I,J:],K:] = dom f & 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 u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & 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 u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )
A4: dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )
then consider r being Real such that
A5: ( 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 A2, A3, Th8;
take r ; :: thesis: ( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )
thus 0 < r by A5; :: thesis: for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e
let u1, u2 be Element of [:REAL,REAL:]; :: thesis: for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e
let x1, y1, x2, y2 be Real; :: thesis: ( u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] implies for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e )
assume A6: ( u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] ) ; :: thesis: for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e
let z be Element of REAL ; :: thesis: ( z in K implies |.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e )
A7: ( x1 in I & x2 in I & y1 in J & y2 in J ) by A6, ZFMISC_1:87;
assume A8: z in K ; :: thesis: |.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e
|.(z - z).| < r by A5;
then |.((g . [x2,y2,z]) - (g . [x1,y1,z])).| < e by A5, A6, A7, A8;
then A9: |.((g . [u2,z]) - (g . [u1,z])).| < e by A6;
a9: (g . [u2,z]) - (g . [u1,z]) = (g . [u2,z]) - (g . [u1,z]) ;
( (ProjPMap1 ((R_EAL g),u1)) . z = (R_EAL g) . (u1,z) & (R_EAL g) . (u1,z) = g . [u1,z] & (ProjPMap1 ((R_EAL g),u2)) . z = (R_EAL g) . (u2,z) & (R_EAL g) . (u2,z) = g . [u2,z] ) by A4, A6, A8, ZFMISC_1:87, MESFUNC5:def 7, MESFUN12:def 3;
hence |.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e by A9, a9, EXTREAL1:12; :: thesis: verum