let X, Y be set ; :: thesis: for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )
let f be Function of X,Y; :: thesis: ( f is onto iff [:f,f:] is onto )
rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67;
then ( rng f = Y iff rng [:f,f:] = [:Y,Y:] ) by ZFMISC_1:92;
hence ( f is onto iff [:f,f:] is onto ) ; :: thesis: verum