for X being set
for T being Element of TOL X holds
( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T ) ;