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 Element of X st 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 Element of X st y = f . x
let f be Function of X,Y; :: thesis: ( f is onto implies for y being Element of Y ex x being Element of X st y = f . x )
assume A1: f is onto ; :: thesis: for y being Element of Y ex x being Element of X st y = f . x
let y be Element of Y; :: thesis: ex x being Element of X st y = f . x
ex x being object st
( x in X & f . x = y ) by A1, Th1;
hence ex x being Element of X st y = f . x ; :: thesis: verum