per cases ( not D is empty or D is empty ) ;
suppose not D is empty ; :: thesis: ex b1 being BinOp of D st b1 is associative
then reconsider DD = D as non empty set ;
set f = DD -pr1 ;
reconsider ff = DD -pr1 as BinOp of D ;
take ff ; :: thesis: ff is associative
thus ff is associative ; :: thesis: verum
end;
suppose D is empty ; :: thesis: ex b1 being BinOp of D st b1 is associative
then reconsider DD = D as empty set ;
set f = the BinOp of {};
( the BinOp of {} is associative & the BinOp of {} is BinOp of DD ) ;
hence ex b1 being BinOp of D st b1 is associative ; :: thesis: verum
end;
end;