let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f being Functional of V holds f - f = 0Functional V
let V be non empty ModuleStr over K; :: thesis: for f being Functional of V holds f - f = 0Functional V
let f be Functional of V; :: thesis: f - f = 0Functional V

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

let x be Element of V; :: thesis: (f - f) . x = (0Functional V) . x
thus (f - f) . x = (f . x) + ((- f) . x) by Def3
.= (f . x) + (- (f . x)) by Def4
.= 0. K by RLVECT_1:5
.= (0Functional V) . x by FUNCOP_1:7 ; :: thesis: verum

end;

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