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 A1: f is onto ; :: thesis: for y being Element of Y ex x being set st
( x in X & y = f . x )
let y be Element of Y; :: thesis: ex x being set st
( x in X & y = f . x )
rng f = Y by A1, FUNCT_2:def 3;
hence ex x being set st
( x in X & y = f . x ) by FUNCT_2:17; :: thesis: verum