let V be non empty ModuleStr over INT.Ring ; :: thesis: for f being FrFunctional of V holds f + (0FrFunctional V) = f
let f be FrFunctional of V; :: thesis: f + (0FrFunctional V) = f

now :: thesis: for x being Element of V holds (f + (0FrFunctional V)) . x = f . x

let x be Element of V; :: thesis: (f + (0FrFunctional V)) . x = f . x
thus (f + (0FrFunctional V)) . x = (f . x) + ((0FrFunctional V) . x) by HDef3
.= (f . x) + (0. F_Real) by FUNCOP_1:7
.= f . x ; :: thesis: verum

end;

hence f + (0FrFunctional V) = f by FUNCT_2:63; :: thesis: verum