for X being set
for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )