let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.g.|,z) holds
p2 is_continuous_on dom p2
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.g.|,z) holds
p2 is_continuous_on dom p2
let p2 be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for z being Element of REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.g.|,z) holds
p2 is_continuous_on dom p2
let z be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.g.|,z) implies p2 is_continuous_on dom p2 )
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: p2 = ProjPMap2 (|.g.|,z) ; :: thesis: p2 is_continuous_on dom p2
reconsider q2 = ProjPMap2 (g,z) as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A4: q2 is_continuous_on dom q2 by A1, A2, Th12;
A5: ProjPMap2 (|.g.|,z) = |.(ProjPMap2 (g,z)).| by MESFUN16:32;
then p2 = ||.q2.|| by A3, MESFUN16:19;
then p2 is_continuous_on dom q2 by A4, MESFUN16:22;
hence p2 is_continuous_on dom p2 by A3, A5, VALUED_1:def 11; :: thesis: verum