let V be non empty ModuleStr over INT.Ring ; :: thesis: for f, g being FrFunctional of V holds f + g = g + f
let f, g be FrFunctional 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 HDef3
.= (g + f) . x by HDef3 ; :: thesis: verum

end;

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