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;
then Pf2 = R_EAL (abs (ProjPMap2 (g,z))) by MESFUNC6:1;
then Pf2 = R_EAL (ProjPMap2 (|.g.|,z)) by MESFUN16:32;
hence Pf2 is_continuous_on dom Pf2 by A1, A2, Th14, MESFUNC5:def 7; :: thesis: verum