let z 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
for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) holds
Pf2 is_continuous_on dom Pf2
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) holds
Pf2 is_continuous_on dom Pf2
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) holds
Pf2 is_continuous_on dom Pf2
let Pf2 be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: ( f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) implies Pf2 is_continuous_on dom Pf2 )
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pf2 = ProjPMap2 ((R_EAL g),z) ; :: thesis: Pf2 is_continuous_on dom Pf2
Pf2 = R_EAL (ProjPMap2 (g,z)) by A3, MESFUN16:31;
hence Pf2 is_continuous_on dom Pf2 by A1, A2, Th12, MESFUNC5:def 7; :: thesis: verum