for A being set
for B being non empty set
for f being Function of A,B holds [:f,f:] .: (id A) c= id B