let X be non empty set ; :: thesis: for L being non empty right-distributive doubleLoopStr
for a being Element of L
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)
let L be non empty right-distributive doubleLoopStr ; :: thesis: for a being Element of L
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)
let a be Element of L; :: thesis: for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)
let f, g be Function of X,L; :: thesis: a '*' (f '+' g) = (a '*' f) '+' (a '*' g)

now :: thesis: for o being object st o in X holds
(a '*' (f '+' g)) . o = ((a '*' f) '+' (a '*' g)) . o

let o be object ; :: thesis: ( o in X implies (a '*' (f '+' g)) . o = ((a '*' f) '+' (a '*' g)) . o )
assume o in X ; :: thesis: (a '*' (f '+' g)) . o = ((a '*' f) '+' (a '*' g)) . o
then reconsider x = o as Element of X ;
thus (a '*' (f '+' g)) . o = a * ((f '+' g) . x) by defmu
.= a * ((f . x) + (g . x)) by defp
.= (a * (f . x)) + (a * (g . x)) by VECTSP_1:def 2
.= (a * (f . x)) + ((a '*' g) . x) by defmu
.= ((a '*' f) . x) + ((a '*' g) . x) by defmu
.= ((a '*' f) '+' (a '*' g)) . o by defp ; :: thesis: verum

end;

hence a '*' (f '+' g) = (a '*' f) '+' (a '*' g) by FUNCT_2:12; :: thesis: verum