let X be non empty set ; :: thesis: id X is dneg
set f = id X;
for x being Element of X holds (id X) . ((id X) . x) = x

proof

let a be Element of X; :: thesis: (id X) . ((id X) . a) = a
(id X) . a = a by FUNCT_1:34;
hence (id X) . ((id X) . a) = a ; :: thesis: verum

end;

hence id X is dneg by Def3; :: thesis: verum