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;