let A, B, C be set ; :: thesis: for f being Function of [:A,B:],C st ~ f is onto holds
f is onto
let f be Function of [:A,B:],C; :: thesis: ( ~ f is onto implies f is onto )
A1: rng (~ f) c= rng f by FUNCT_4:41;
assume ~ f is onto ; :: thesis: f is onto
then rng (~ f) = C ;
hence rng f = C by A1; :: according to FUNCT_2:def 3 :: thesis: verum