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