let K be non empty right-distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
let V, W be non empty VectSpStr of K; :: thesis: for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
let r be Element of K; :: 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

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 Def4
.= r * ((f . (v,w)) + (g . (v,w))) by Def3
.= (r * (f . (v,w))) + (r * (g . (v,w))) by VECTSP_1:def 2
.= ((r * f) . (v,w)) + (r * (g . (v,w))) by Def4
.= ((r * f) . (v,w)) + ((r * g) . (v,w)) by Def4
.= ((r * f) + (r * g)) . (v,w) by Def3 ; :: thesis: verum

end;

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