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