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 P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) holds
P2 is_continuous_on dom P2
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 P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) holds
P2 is_continuous_on dom P2
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) holds
P2 is_continuous_on dom P2
let P2 be PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real; :: thesis: for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) holds
P2 is_continuous_on dom P2
let q be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) 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.|,q) ; :: thesis: P2 is_continuous_on dom P2
reconsider P1 = ProjPMap2 (g,q) as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real by MEASUR15:42;
A4: P1 is_continuous_on dom P1 by A1, A2, Th16;
dom P1 = dom |.(ProjPMap2 (g,q)).| by VALUED_1:def 11;
then A5: dom P1 = dom P2 by A3, MESFUN16:32;
for x0 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x0 in dom P2 holds
P2 is_continuous_in x0

proof

let x0 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( x0 in dom P2 implies P2 is_continuous_in x0 )
assume A6: x0 in dom P2 ; :: thesis: P2 is_continuous_in x0
reconsider yy = q as Point of RNS_Real ;
reconsider p0 = [x0,yy] as Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] ;
A7: P1 is_continuous_in x0 by A4, A5, A6;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & ||.(x1 - x0).|| < s holds
||.((P2 /. x1) - (P2 /. x0)).|| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & ||.(x1 - x0).|| < s holds
||.((P2 /. x1) - (P2 /. x0)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & ||.(x1 - x0).|| < s holds
||.((P2 /. x1) - (P2 /. x0)).|| < r ) )
then consider s0 being Real such that
A8: 0 < s0 and
A9: for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P1 & ||.(x1 - x0).|| < s0 holds
||.((P1 /. x1) - (P1 /. x0)).|| < r by A7, NFCONT_1:7;

now :: thesis: for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & ||.(x1 - x0).|| < s0 holds
||.((P2 /. x1) - (P2 /. x0)).|| < r

let x1 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( x1 in dom P2 & ||.(x1 - x0).|| < s0 implies ||.((P2 /. x1) - (P2 /. x0)).|| < r )
assume that
A10: x1 in dom P2 and
A11: ||.(x1 - x0).|| < s0 ; :: thesis: ||.((P2 /. x1) - (P2 /. x0)).|| < r
A12: ||.((P1 /. x1) - (P1 /. x0)).|| < r by A5, A9, A10, A11;
reconsider xx1 = x1, xx0 = x0 as Element of CarProduct ((Seg n) --> REAL) by MEASUR15:42;
A13: xx1 in dom |.(ProjPMap2 (g,q)).| by A10, A3, MESFUN16:32;
A14: xx0 in dom |.(ProjPMap2 (g,q)).| by A6, A3, MESFUN16:32;
A15: P1 /. x1 = (ProjPMap2 (g,q)) . xx1 by A5, A10, PARTFUN1:def 6;
(ProjPMap2 (|.g.|,q)) . xx1 = |.(ProjPMap2 (g,q)).| . xx1 by MESFUN16:32;
then P2 /. x1 = |.(ProjPMap2 (g,q)).| . xx1 by A3, A10, PARTFUN1:def 6;
then P2 /. x1 = |.((ProjPMap2 (g,q)) . xx1).| by A13, VALUED_1:def 11;
then A16: P2 /. x1 = ||.(P1 /. x1).|| by A15, EUCLID:def 2;
A17: P1 /. x0 = (ProjPMap2 (g,q)) . xx0 by A5, A6, PARTFUN1:def 6;
(ProjPMap2 (|.g.|,q)) . xx0 = |.(ProjPMap2 (g,q)).| . xx0 by MESFUN16:32;
then P2 /. x0 = |.(ProjPMap2 (g,q)).| . xx0 by A3, A6, PARTFUN1:def 6;
then P2 /. x0 = |.((ProjPMap2 (g,q)) . xx0).| by A14, VALUED_1:def 11;
then P2 /. x0 = ||.(P1 /. x0).|| by A17, EUCLID:def 2;
then (P2 /. x1) - (P2 /. x0) = ||.(P1 /. x1).|| - ||.(P1 /. x0).|| by A16, DUALSP03:4;
then ||.((P2 /. x1) - (P2 /. x0)).|| = |.(||.(P1 /. x1).|| - ||.(P1 /. x0).||).| by EUCLID:def 2;
then ||.((P2 /. x1) - (P2 /. x0)).|| <= ||.((P1 /. x1) - (P1 /. x0)).|| by NORMSP_1:9;
hence ||.((P2 /. x1) - (P2 /. x0)).|| < r by A12, XXREAL_0:2; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & ||.(x1 - x0).|| < s holds
||.((P2 /. x1) - (P2 /. x0)).|| < r ) ) by A8; :: thesis: verum

end;

hence P2 is_continuous_in x0 by A6, NFCONT_1:7; :: thesis: verum

end;

hence P2 is_continuous_on dom P2 ; :: thesis: verum