thus ( G is associative implies the multF of G is associative ) :: thesis: ( the multF of G is associative implies G is associative )

proof

assume A3: for a, b, c being Element of G holds (a * b) * c = a * (b * c) ; :: according to GROUP_1:def 4 :: thesis: the multF of G is associative
let a be Element of G; :: according to BINOP_1:def 14 :: 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 A3; :: thesis: verum

end;

assume A4: 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 :: thesis: G is associative
let a be Element of G; :: according to GROUP_1:def 4 :: thesis: for b₁, b₂ being Element of the carrier of G holds (a [*] b₁) [*] b₂ = a [*] (b₁ [*] b₂)
let b, c be Element of G; :: thesis: (a [*] b) [*] c = a [*] (b [*] c)
thus (a [*] b) [*] c = a [*] (b [*] c) by A4; :: thesis: verum