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

suppose not D is empty ; :: thesis: ex b₁ being BinOp of D st b₁ 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 b₁ being BinOp of D st b₁ 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 b₁ being BinOp of D st b₁ is associative ; :: thesis: verum

end;

end;