let K be non empty Abelian addLoopStr ; :: thesis: for V being non empty VectSpStr of K
for f, g being Functional of V holds f + g = g + f
let V be non empty VectSpStr of 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

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

end;

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