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