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