let X be set ; :: thesis: 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 set st
( x in X & y = f . x )
let Y be non empty set ; :: thesis: for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being set st
( x in X & y = f . x )
let f be Function of X,Y; :: thesis: ( f is onto implies for y being Element of Y ex x being set st
( x in X & y = f . x ) )
assume f is onto ; :: thesis: for y being Element of Y ex x being set st
( x in X & y = f . x )
then A1: rng f = Y by FUNCT_2:def 3;
let y be Element of Y; :: thesis: ex x being set st
( x in X & y = f . x )
thus ex x being set st
( x in X & y = f . x ) by A1, FUNCT_2:11; :: thesis: verum