let X be non empty set ; :: thesis: for R being Ring
for L being non empty scalar-distributive ModuleStr over R
for a, b being Element of R
for f being Function of X,L holds (a + b) '*' f = (a '*' f) '+' (b '*' f)
let F be Ring; :: thesis: for L being non empty scalar-distributive ModuleStr over F
for a, b being Element of F
for f being Function of X,L holds (a + b) '*' f = (a '*' f) '+' (b '*' f)
let L be non empty scalar-distributive ModuleStr over F; :: thesis: for a, b being Element of F
for f being Function of X,L holds (a + b) '*' f = (a '*' f) '+' (b '*' f)
let a, b be Element of F; :: 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 15
.= ((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