let K be non empty right_zeroed addLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f being Functional of V holds f + (0Functional V) = f
let V be non empty ModuleStr over K; :: thesis: for f being Functional of V holds f + (0Functional V) = f
let f be Functional of V; :: thesis: f + (0Functional V) = f

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

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

end;

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