let K be non empty right-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over 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 ModuleStr over 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)

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 ModuleStr over 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 :: 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)

hence
r * (f + g) = (r * f) + (r * g)
; :: thesis: verumfor 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 Def3

.= r * ((f . (v,w)) + (g . (v,w))) by Def2

.= (r * (f . (v,w))) + (r * (g . (v,w))) by VECTSP_1:def 2

.= ((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 ; :: thesis: verum

end;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 Def3

.= r * ((f . (v,w)) + (g . (v,w))) by Def2

.= (r * (f . (v,w))) + (r * (g . (v,w))) by VECTSP_1:def 2

.= ((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 ; :: thesis: verum