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 11
.= ((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