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
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 A4: x0 in dom P2 ; :: thesis: P2 is_continuous_in x0
then A5: x0 in Y-section ((dom g),q) by A3, MESFUN12:def 4;
A6: Y-section ((dom g),q) = { x where x is Element of CarProduct ((Seg n) --> REAL) : [x,q] in dom g } by MEASUR11:def 5;
then A7: ex x being Element of CarProduct ((Seg n) --> REAL) st
( x = x0 & [x,q] in dom g ) by A5;
reconsider yy = q as Point of RNS_Real ;
reconsider xx0 = x0 as Point of (CarProduct ((Seg n) --> RNS_Real)) ;
reconsider p0 = [xx0,yy] as Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] ;
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 p1 being Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st p1 in dom f & ||.(p1 - p0).|| < s0 holds
||.((f /. p1) - (f /. p0)).|| < r by A1, A2, A7, NFCONT_1:19;

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
x1 in Y-section ((dom g),q) by A3, A10, MESFUN12:def 4;
then A12: ex x being Element of CarProduct ((Seg n) --> REAL) st
( x = x1 & [x,q] in dom g ) by A6;
reconsider xx1 = x1 as Point of (CarProduct ((Seg n) --> RNS_Real)) ;
reconsider p1 = [xx1,yy] as Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] ;
p1 - p0 = [xx1,yy] + [(- xx0),(- yy)] by PRVECT_3:18;
then p1 - p0 = [(xx1 - xx0),(yy - yy)] by PRVECT_3:18;
then p1 - p0 = [(xx1 - xx0),(0. RNS_Real)] by RLVECT_1:15;
then ||.(p1 - p0).|| = sqrt ((||.(0. RNS_Real).|| ^2) + (||.(xx1 - xx0).|| ^2)) by NDIFF_8:1;
then A13: ||.(p1 - p0).|| = ||.(xx1 - xx0).|| by SQUARE_1:22;
( P2 . x1 = g . (x1,q) & P2 . x0 = g . (x0,q) ) by A3, A7, A12, MESFUN12:def 4;
then ( P2 . x1 = f /. p1 & P2 . x0 = f /. p0 ) by A2, A7, A12, PARTFUN1:def 6;
then ( P2 /. x1 = f /. p1 & P2 /. x0 = f /. p0 ) by A4, A10, PARTFUN1:def 6;
hence ||.((P2 /. x1) - (P2 /. x0)).|| < r by A11, A2, A12, A9, A13; :: 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 A4, NFCONT_1:7; :: thesis: verum

end;

hence P2 is_continuous_on dom P2 ; :: thesis: verum