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

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

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

end;

hence f1 = g1 by A3, A5, PARTFUN2:1; :: thesis: verum