let X be non empty set ; :: thesis: for L being non empty associative multLoopStr
for a, b being Element of L
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let L be non empty associative multLoopStr ; :: thesis: for a, b being Element of L
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)
let a, b be Element of L; :: 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 GROUP_1:def 3
.= 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