let X be non empty set ; :: thesis: for T being non empty associative multMagma
for f, g, h being Function of X,T holds (f (#) g) (#) h = f (#) (g (#) h)
let T be non empty associative multMagma ; :: thesis: for f, g, h being Function of X,T holds (f (#) g) (#) h = f (#) (g (#) h)
let f, g, h be Function of X,T; :: thesis: (f (#) g) (#) h = f (#) (g (#) h)
let x be Element of X; :: according to FUNCT_2:def 8 :: thesis: ((f (#) g) (#) h) . x = (f (#) (g (#) h)) . x
thus ((f (#) g) (#) h) . x = ((f (#) g) . x) * (h . x) by Def2
.= ((f . x) * (g . x)) * (h . x) by Def2
.= (f . x) * ((g . x) * (h . x)) by GROUP_1:def 3
.= (f . x) * ((g (#) h) . x) by Def2
.= (f (#) (g (#) h)) . x by Def2 ; :: thesis: verum