for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a)