let D be non empty set ; for o being BinOp of D st o is associative holds
o .:^2 is associative
let o be BinOp of D; ( o is associative implies o .:^2 is associative )
assume A1:
o is associative
; o .:^2 is associative
let x, y, z be Subset of D; BINOP_1:def 3 (o .:^2) . (x,((o .:^2) . (y,z))) = (o .:^2) . (((o .:^2) . (x,y)),z)
thus (o .:^2) . (((o .:^2) . (x,y)),z) =
(o .:^2) . ((o .: [:x,y:]),z)
by Th44
.=
o .: [:(o .: [:x,y:]),z:]
by Th44
.=
o .: [:x,(o .: [:y,z:]):]
by A1, Th48
.=
(o .:^2) . (x,(o .: [:y,z:]))
by Th44
.=
(o .:^2) . (x,((o .:^2) . (y,z)))
by Th44
; verum