A1: ( dom (f + 0) = dom f & ( for c being object st c in dom (f + 0) holds
(f + 0) . c = (f . c) + 0 ) ) by VALUED_1:def 2;
for c being object st c in dom (f + 0) holds
(f + 0) . c = f . c

proof

let c be object ; :: thesis: ( c in dom (f + 0) implies (f + 0) . c = f . c )
assume B1: c in dom (f + 0) ; :: thesis: (f + 0) . c = f . c
(f + 0) . c = (f . c) + 0 by VALUED_1:def 2, B1
.= f . c ;
hence (f + 0) . c = f . c ; :: thesis: verum

end;

hence f + 0 = f by A1, FUNCT_1:2; :: thesis: verum