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

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

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

end;

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