let n be non zero Nat; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
Pg2 is_continuous_on dom Pg2
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
Pg2 is_continuous_on dom Pg2
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for Pg2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
Pg2 is_continuous_on dom Pg2
let Pg2 be PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real; :: thesis: for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
Pg2 is_continuous_on dom Pg2
let y be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) implies Pg2 is_continuous_on dom Pg2 )
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: Pg2 = ProjPMap2 (|.(R_EAL g).|,y) ; :: thesis: Pg2 is_continuous_on dom Pg2
Pg2 = |.(R_EAL (ProjPMap2 (g,y))).| by A3, MESFUN16:31;
then Pg2 = R_EAL (abs (ProjPMap2 (g,y))) by MESFUNC6:1;
then Pg2 = R_EAL (ProjPMap2 (|.g.|,y)) by MESFUN16:32;
hence Pg2 is_continuous_on dom Pg2 by A1, A2, Th19, MESFUNC5:def 7; :: thesis: verum