set f = binop D;
thus binop D is associative :: thesis: binop D is commutative

proof

let a, b, c be Element of D; :: according to BINOP_1:def 3 :: thesis: (binop D) . (a,((binop D) . (b,c))) = (binop D) . (((binop D) . (a,b)),c)

per cases ( not D is empty or D is empty ) ;

suppose A1: not D is empty ; :: thesis: (binop D) . (a,((binop D) . (b,c))) = (binop D) . (((binop D) . (a,b)),c)

hence (binop D) . (a,((binop D) . (b,c))) = the Element of D by ZFMISC_1:87, FUNCOP_1:7
.= (binop D) . (((binop D) . (a,b)),c) by A1, ZFMISC_1:87, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose A2: D is empty ; :: thesis: (binop D) . (a,((binop D) . (b,c))) = (binop D) . (((binop D) . (a,b)),c)

hence (binop D) . (a,((binop D) . (b,c))) = {}
.= (binop D) . (((binop D) . (a,b)),c) by A2 ;
:: thesis: verum

end;

end;

end;

let a, b be Element of D; :: according to BINOP_1:def 2 :: thesis: (binop D) . (a,b) = (binop D) . (b,a)

per cases ( not D is empty or D is empty ) ;

suppose A3: not D is empty ; :: thesis: (binop D) . (a,b) = (binop D) . (b,a)

hence (binop D) . (a,b) = the Element of D by ZFMISC_1:87, FUNCOP_1:7
.= (binop D) . (b,a) by A3, ZFMISC_1:87, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose A4: D is empty ; :: thesis: (binop D) . (a,b) = (binop D) . (b,a)

hence (binop D) . (a,b) = {}
.= (binop D) . (b,a) by A4 ;
:: thesis: verum

end;

end;