let D be non empty set ; :: thesis: for o being BinOp of D st o is associative holds
o .:^2 is associative
let o be BinOp of D; :: thesis: ( o is associative implies o .:^2 is associative )
assume A1: o is associative ; :: thesis: o .:^2 is associative
let x, y, z be Subset of D; :: according to BINOP_1:def 14 :: thesis: (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 Th45
.= o .: [:(o .: [:x,y:]),z:] by Th45
.= o .: [:x,(o .: [:y,z:]):] by A1, Th49
.= (o .:^2) . (x,(o .: [:y,z:])) by Th45
.= (o .:^2) . (x,((o .:^2) . (y,z))) by Th45 ; :: thesis: verum