theorem Th1: :: JORDAN1K:1

for X being set
for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being object st
( x in X & y = f . x ) by FUNCT_2:11;