let G be non empty multMagma ; :: thesis: ( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
thus ( G is associative implies for a, b, c being Element of G holds (a * b) * c = a * (b * c) ) :: thesis: ( ( for a, b, c being Element of G holds (a * b) * c = a * (b * c) ) implies G is associative )

proof

assume A1: for a, b, c being Element of G holds H₂(G) . a,(H₂(G) . b,c) = H₂(G) . (H₂(G) . a,b),c ; :: according to BINOP_1:def 14,MONOID_0:def 12 :: thesis: for a, b, c being Element of G holds (a * b) * c = a * (b * c)
let a, b, c be Element of G; :: thesis: (a * b) * c = a * (b * c)
thus (a * b) * c = a * (b * c) by A1; :: thesis: verum

end;

assume A2: for a, b, c being Element of G holds (a * b) * c = a * (b * c) ; :: thesis: G is associative
let a be Element of G; :: according to BINOP_1:def 14,MONOID_0:def 12 :: thesis: for b₁, b₂ being Element of the carrier of G holds the multF of G . a,(the multF of G . b₁,b₂) = the multF of G . (the multF of G . a,b₁),b₂
let b, c be Element of G; :: thesis: the multF of G . a,(the multF of G . b,c) = the multF of G . (the multF of G . a,b),c
( H₂(G) . (a * b),c = (a * b) * c & H₂(G) . a,(b * c) = a * (b * c) ) ;
hence the multF of G . a,(the multF of G . b,c) = the multF of G . (the multF of G . a,b),c by A2; :: thesis: verum