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 p being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g holds
ProjPMap1 (|.g.|,p) is continuous
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 p being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g holds
ProjPMap1 (|.g.|,p) is continuous
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for p being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g holds
ProjPMap1 (|.g.|,p) is continuous
let p be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( f is_continuous_on dom f & f = g implies ProjPMap1 (|.g.|,p) is continuous )
assume that
A1: f is_continuous_on dom f and
A2: f = g ; :: thesis: ProjPMap1 (|.g.|,p) is continuous
set Y = dom (ProjPMap1 (g,p));
(ProjPMap1 (g,p)) | (dom (ProjPMap1 (g,p))) is continuous by A1, A2, Th14;
then (abs (ProjPMap1 (g,p))) | (dom (ProjPMap1 (g,p))) is continuous by FCONT_1:21;
hence ProjPMap1 (|.g.|,p) is continuous by MESFUN16:32; :: thesis: verum