let V be non empty ModuleStr over INT.Ring ; :: thesis: for f, g, h being FrFunctional of V holds (f + g) + h = f + (g + h)
let f, g, h be FrFunctional of V; :: thesis: (f + g) + h = f + (g + h)
now :: thesis: for x being Element of V holds ((f + g) + h) . x = (f + (g + h)) . x
let x be Element of V; :: thesis: ((f + g) + h) . x = (f + (g + h)) . x
thus ((f + g) + h) . x = ((f + g) . x) + (h . x) by HDef3
.= ((f . x) + (g . x)) + (h . x) by HDef3
.= (f . x) + ((g . x) + (h . x))
.= (f . x) + ((g + h) . x) by HDef3
.= (f + (g + h)) . x by HDef3 ; :: thesis: verum
end;
hence (f + g) + h = f + (g + h) by FUNCT_2:63; :: thesis: verum