let f, g be FrForm of V,W; f + g = g + f
now for v being Vector of V
for w being Vector of W holds (f + g) . (v,w) = (g + f) . (v,w)let v be
Vector of
V;
for w being Vector of W holds (f + g) . (v,w) = (g + f) . (v,w)let w be
Vector of
W;
(f + g) . (v,w) = (g + f) . (v,w)thus (f + g) . (
v,
w) =
(f . (v,w)) + (g . (v,w))
by Def2
.=
(g + f) . (
v,
w)
by Def2
;
verum end;
hence
f + g = g + f
; verum