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:88;
then ( rng f = Y iff rng [:f,f:] = [:Y,Y:] ) by ZFMISC_1:115;
hence ( f is onto iff [:f,f:] is onto ) by FUNCT_2:def 3; :: thesis: verum