let V, W be non empty ModuleStr over INT.Ring ; for f being Form of V,W holds f - f = NulForm (V,W)
let f be Form of V,W; f - f = NulForm (V,W)
now for v being Vector of V
for w being Vector of W holds (f - f) . (v,w) = (NulForm (V,W)) . (v,w)let v be
Vector of
V;
for w being Vector of W holds (f - f) . (v,w) = (NulForm (V,W)) . (v,w)let w be
Vector of
W;
(f - f) . (v,w) = (NulForm (V,W)) . (v,w)thus (f - f) . (
v,
w) =
(f . (v,w)) - (f . (v,w))
by BLDef7
.=
(NulForm (V,W)) . (
v,
w)
by FUNCOP_1:70
;
verum end;
hence
f - f = NulForm (V,W)
; verum