let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of CNS,CNS st f = id (dom f) holds
f is_continuous_on dom f
let f be PartFunc of CNS,CNS; :: 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 CNS st x0 in dom f holds
f /. x0 = x0

let x0 be Point of CNS; :: 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 Th128; :: thesis: verum