let K be non empty Abelian addLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f, g being Functional of V holds f + g = g + f
let V be non empty ModuleStr over K; :: thesis: for f, g being Functional of V holds f + g = g + f
let f, g be Functional of V; :: thesis: f + g = g + f

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

let x be Element of V; :: thesis: (f + g) . x = (g + f) . x
thus (f + g) . x = (f . x) + (g . x) by Def3
.= (g + f) . x by Def3 ; :: thesis: verum

end;

hence f + g = g + f by FUNCT_2:63; :: thesis: verum