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

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 Th149; :: thesis: verum