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