let A be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is associative holds
o,D .: A is associative
let D be non empty set ; :: thesis: for o being BinOp of D st o is associative holds
o,D .: A is associative
let o be BinOp of D; :: thesis: ( o is associative implies o,D .: A is associative )
assume A1: o is associative ; :: thesis: o,D .: A is associative
set F = o,D .: A;
let f, g, h be Element of Funcs A,D; :: according to BINOP_1:def 14 :: thesis: (o,D .: A) . f,((o,D .: A) . g,h) = (o,D .: A) . ((o,D .: A) . f,g),h
thus (o,D .: A) . ((o,D .: A) . f,g),h = (o,D .: A) . (o .: f,g),h by Def2
.= o .: (o .: f,g),h by Def2
.= o .: f,(o .: g,h) by A1, Th5
.= (o,D .: A) . f,(o .: g,h) by Def2
.= (o,D .: A) . f,((o,D .: A) . g,h) by Def2 ; :: thesis: verum