let S be RealNormSpace; :: thesis: for f being PartFunc of S,S st f = id (dom f) holds
f is_continuous_on dom f
let f be PartFunc of S,S; :: thesis: ( f = id (dom f) implies f is_continuous_on dom f )
assume A1: f = id (dom f) ; :: thesis: f is_continuous_on dom f
now :: thesis: for x0 being Point of S st x0 in dom f holds
f /. x0 = x0
let x0 be Point of S; :: thesis: ( x0 in dom f implies f /. x0 = x0 )
assume A2: x0 in dom f ; :: thesis: f /. x0 = x0
thus f /. x0 = f . x0 by A2, PARTFUN1:def 6
.= x0 by A1, A2, FUNCT_1:17 ; :: thesis: verum
end;
hence f is_continuous_on dom f by Th49; :: thesis: verum