thus ( G is associative implies the multF of G is associative ) ; :: thesis: ( the multF of G is associative implies G is associative )
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 3 :: 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