let f be Function; :: thesis: ( rng f = dom f implies f is onto Function of (dom f),(dom f) )
set D = dom f;
set C = rng f;
reconsider ff = f as Element of Funcs ((dom f),(rng f)) by FUNCT_2:def 2;
assume A1: rng f = dom f ; :: thesis: f is onto Function of (dom f),(dom f)
then reconsider fff = ff as Function of (dom f),(dom f) by FUNCT_2:66;
( fff is onto & fff is dom f -valued ) by FUNCT_2:def 3, A1;
hence f is onto Function of (dom f),(dom f) ; :: thesis: verum