let V, W be non empty ModuleStr over INT.Ring ; for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)
let f, g, h be Form of V,W; (f + g) + h = f + (g + h)
now for v being Vector of V
for w being Vector of W holds ((f + g) + h) . (v,w) = (f + (g + h)) . (v,w)let v be
Vector of
V;
for w being Vector of W holds ((f + g) + h) . (v,w) = (f + (g + h)) . (v,w)let w be
Vector of
W;
((f + g) + h) . (v,w) = (f + (g + h)) . (v,w)thus ((f + g) + h) . (
v,
w) =
((f + g) . (v,w)) + (h . (v,w))
by BLDef2
.=
((f . (v,w)) + (g . (v,w))) + (h . (v,w))
by BLDef2
.=
(f . (v,w)) + ((g . (v,w)) + (h . (v,w)))
.=
(f . (v,w)) + ((g + h) . (v,w))
by BLDef2
.=
(f + (g + h)) . (
v,
w)
by BLDef2
;
verum end;
hence
(f + g) + h = f + (g + h)
; verum