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 3 :: 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 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 ; :: thesis: verum