let V, W be non empty ModuleStr over INT.Ring ; for a being Element of F_Real
for f, g being FrForm of V,W holds a * (f + g) = (a * f) + (a * g)
let r be Element of F_Real; for f, g being FrForm of V,W holds r * (f + g) = (r * f) + (r * g)
let f, g be FrForm of V,W; r * (f + g) = (r * f) + (r * g)
now for v being Vector of V
for w being Vector of W holds (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)let v be
Vector of
V;
for w being Vector of W holds (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)let w be
Vector of
W;
(r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)thus (r * (f + g)) . (
v,
w) =
r * ((f + g) . (v,w))
by Def3
.=
r * ((f . (v,w)) + (g . (v,w)))
by Def2
.=
(r * (f . (v,w))) + (r * (g . (v,w)))
.=
((r * f) . (v,w)) + (r * (g . (v,w)))
by Def3
.=
((r * f) . (v,w)) + ((r * g) . (v,w))
by Def3
.=
((r * f) + (r * g)) . (
v,
w)
by Def2
;
verum end;
hence
r * (f + g) = (r * f) + (r * g)
; verum