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 ) )
dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
then A4: dom |.(R_EAL g).| = [:[:I,J:],K:] by MESFUNC1:def 10;
A5: for x being Element of [:REAL,REAL:]
for y being Element of REAL st x in [:I,J:] & y in K holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

let x be Element of [:REAL,REAL:]; :: thesis: for y being Element of REAL st x in [:I,J:] & y in K holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
let y be Element of REAL ; :: thesis: ( x in [:I,J:] & y in K implies ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] ) )
assume A6: ( x in [:I,J:] & y in K ) ; :: thesis: ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
hence (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) by A4, ZFMISC_1:87, MESFUN12:def 3; :: thesis: |.(R_EAL g).| . (x,y) = |.g.| . [x,y]
[x,y] in dom g by A6, A1, A3, ZFMISC_1:87;
then A7: [x,y] in dom |.g.| by VALUED_1:def 11;
A8: (R_EAL g) . [x,y] = g . [x,y] by MESFUNC5:def 7;
|.(R_EAL g).| . (x,y) = |.((R_EAL g) . [x,y]).| by A4, A6, ZFMISC_1:87, MESFUNC1:def 10;
then |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| by A8, EXTREAL1:12;
hence |.(R_EAL g).| . (x,y) = |.g.| . [x,y] by VALUED_1:def 11, A7; :: thesis: verum

end;

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
A9: ( 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, Th10;
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 A9; :: 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 A10: ( 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 )
A11: ( x1 in I & x2 in I & y1 in J & y2 in J ) by A10, ZFMISC_1:87;
assume A12: z in K ; :: thesis: |.(((ProjPMap1 (|.(R_EAL g).|,u2)) . z) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . z)).| < e
|.(z - z).| < r by A9;
then |.((|.g.| . [x2,y2,z]) - (|.g.| . [x1,y1,z])).| < e by A9, A10, A11, A12;
then A13: |.((|.g.| . [u2,z]) - (|.g.| . [u1,z])).| < e by A10;
a13: (|.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 A5, A10, A12;
hence |.(((ProjPMap1 (|.(R_EAL g).|,u2)) . z) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . z)).| < e by A13, a13, EXTREAL1:12; :: thesis: verum