theorem Th4: :: FUNCTOR0:4

for X, Y being set
for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )