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

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

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

end;

hence f - f = 0FrFunctional V by FUNCT_2:63; :: thesis: verum