theorem Th11: :: FUNCTOR0:11

for A, B being set
for f being Function of A,B st f is onto holds
id B c= [:f,f:] .: (id A)