set X = (dom f) \ (f " {0});
let f, g be PartFunc of C,COMPLEX; :: thesis: ( dom f = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom f holds
f /. c = (f /. c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom g holds
g /. c = (f /. c) " ) implies f = g )
assume that
A3: dom f = (dom f) \ (f " {0}) and
A4: for c being Element of C st c in dom f holds
f /. c = H₁(c) and
A5: dom g = (dom f) \ (f " {0}) and
A6: for c being Element of C st c in dom g holds
g /. c = H₁(c) ; :: thesis: f = g

now :: thesis: for c being Element of C st c in dom f holds
f /. c = g /. c

let c be Element of C; :: thesis: ( c in dom f implies f /. c = g /. c )
assume A7: c in dom f ; :: thesis: f /. c = g /. c
hence f /. c = H₁(c) by A4
.= g /. c by A7, A3, A5, A6 ;
:: thesis: verum

end;

hence f = g by A3, A5, PARTFUN2:1; :: thesis: verum