theorem Th13: :: FUNCTOR0:13

for A, B, C being set
for f being Function of [:A,B:],C st ~ f is onto holds
f is onto