let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for a being Element of INT.Ring
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
let r be Element of INT.Ring; :: thesis: for f, g being Form of V,W holds r * (f + g) = (r * f) + (r * g)
let f, g be Form of V,W; :: thesis: r * (f + g) = (r * f) + (r * g)

now :: thesis: 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; :: thesis: for w being Vector of W holds (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)
let w be Vector of W; :: thesis: (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)
thus (r * (f + g)) . (v,w) = r * ((f + g) . (v,w)) by BLDef3
.= r * ((f . (v,w)) + (g . (v,w))) by BLDef2
.= (r * (f . (v,w))) + (r * (g . (v,w)))
.= ((r * f) . (v,w)) + (r * (g . (v,w))) by BLDef3
.= ((r * f) . (v,w)) + ((r * g) . (v,w)) by BLDef3
.= ((r * f) + (r * g)) . (v,w) by BLDef2 ; :: thesis: verum

end;

hence r * (f + g) = (r * f) + (r * g) ; :: thesis: verum