let K be non empty right-distributive doubleLoopStr ; :: thesis: for V being non empty ModuleStr over K
for r being Element of K
for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)
let V be non empty ModuleStr over K; :: thesis: for r being Element of K
for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)
let r be Element of K; :: thesis: for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)
let f, g be Functional of V; :: thesis: r * (f + g) = (r * f) + (r * g)

now :: thesis: for x being Element of V holds (r * (f + g)) . x = ((r * f) + (r * g)) . x

let x be Element of V; :: thesis: (r * (f + g)) . x = ((r * f) + (r * g)) . x
thus (r * (f + g)) . x = r * ((f + g) . x) by Def6
.= r * ((f . x) + (g . x)) by Def3
.= (r * (f . x)) + (r * (g . x)) by VECTSP_1:def 2
.= ((r * f) . x) + (r * (g . x)) by Def6
.= ((r * f) . x) + ((r * g) . x) by Def6
.= ((r * f) + (r * g)) . x by Def3 ; :: thesis: verum

end;

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