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

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