let S be RealNormSpace; :: thesis: for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds
f /. x0 = ||.x0.|| ) holds
f is_continuous_on dom f
let f be PartFunc of the carrier of S,REAL; :: thesis: ( ( for x0 being Point of S st x0 in dom f holds
f /. x0 = ||.x0.|| ) implies f is_continuous_on dom f )
assume A1: for x0 being Point of S st x0 in dom f holds
f /. x0 = ||.x0.|| ; :: thesis: f is_continuous_on dom f
now :: thesis: for x1, x2 being Point of S st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).||
let x1, x2 be Point of S; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).|| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).||
then ( f /. x1 = ||.x1.|| & f /. x2 = ||.x2.|| ) by A1;
hence |.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).|| by NORMSP_1:9; :: thesis: verum
end;
then f is_Lipschitzian_on dom f ;
hence f is_continuous_on dom f by Th46; :: thesis: verum