let S, T be RealNormSpace; :: thesis: for x being Point of T holds the carrier of S --> x is_continuous_on the carrier of S
let x be Point of T; :: thesis: the carrier of S --> x is_continuous_on the carrier of S

A1: now :: thesis: for x1 being Point of S
for r being Real st x1 in the carrier of S & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r ) )

let x1 be Point of S; :: thesis: for r being Real st x1 in the carrier of S & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r ) )
let r be Real; :: thesis: ( x1 in the carrier of S & 0 < r implies ex s being Real st
( 0 < s & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r ) ) )
assume that
x1 in the carrier of S and
A2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r ) )
take s = r; :: thesis: ( 0 < s & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r ) )
thus 0 < s by A2; :: thesis: for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r
let x2 be Point of S; :: thesis: ( x2 in the carrier of S & ||.(x2 - x1).|| < s implies ||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r )
assume ( x2 in the carrier of S & ||.(x2 - x1).|| < s ) ; :: thesis: ||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r
reconsider xx1 = x1, xx2 = x2 as Point of S ;
( ( the carrier of S --> x) /. xx1 = x & ( the carrier of S --> x) /. xx2 = x ) by FUNCOP_1:7;
hence ||.((( the carrier of S --> x) /. x2) - (( the carrier of S --> x) /. x1)).|| < r by A2, NORMSP_1:6; :: thesis: verum

end;

dom ( the carrier of S --> x) = the carrier of S by FUNCOP_1:13;
hence the carrier of S --> x is_continuous_on the carrier of S by A1, NFCONT_1:19; :: thesis: verum