let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL
for t being Element of REAL st f is_continuous_on dom f & f = g holds
( ProjPMap1 (|.g.|,t) is continuous & ProjPMap2 (|.g.|,t) is continuous )
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: for t being Element of REAL st f is_continuous_on dom f & f = g holds
( ProjPMap1 (|.g.|,t) is continuous & ProjPMap2 (|.g.|,t) is continuous )
let t be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g implies ( ProjPMap1 (|.g.|,t) is continuous & ProjPMap2 (|.g.|,t) is continuous ) )
assume that
A1: f is_continuous_on dom f and
A2: f = g ; :: thesis: ( ProjPMap1 (|.g.|,t) is continuous & ProjPMap2 (|.g.|,t) is continuous )
set Y = dom (ProjPMap1 (g,t));
A3: dom (ProjPMap1 (g,t)) = dom |.(ProjPMap1 (g,t)).| by VALUED_1:def 11;
(ProjPMap1 (g,t)) | (dom (ProjPMap1 (g,t))) is continuous by A1, A2, Th33;
then (abs (ProjPMap1 (g,t))) | (dom (ProjPMap1 (g,t))) is continuous by FCONT_1:21;
hence ProjPMap1 (|.g.|,t) is continuous by A3, Th32; :: thesis: ProjPMap2 (|.g.|,t) is continuous
set Y2 = dom (ProjPMap2 (g,t));
A4: dom (ProjPMap2 (g,t)) = dom |.(ProjPMap2 (g,t)).| by VALUED_1:def 11;
(ProjPMap2 (g,t)) | (dom (ProjPMap2 (g,t))) is continuous by A1, A2, Th33;
then (abs (ProjPMap2 (g,t))) | (dom (ProjPMap2 (g,t))) is continuous by FCONT_1:21;
hence ProjPMap2 (|.g.|,t) is continuous by A4, Th32; :: thesis: verum