let X be non empty set ; :: thesis: for R being Ring
for L being non empty scalar-associative ModuleStr over R
for a, b being Element of R
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let F be Ring; :: thesis: for L being non empty scalar-associative ModuleStr over F
for a, b being Element of F
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let L be non empty scalar-associative ModuleStr over F; :: thesis: for a, b being Element of F
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let a, b be Element of F; :: thesis: for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let f be Function of X,L; :: thesis: (a * b) '*' f = a '*' (b '*' f)

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

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

end;

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