let S, T be RelStr ; :: thesis: for f being Function of S,T st f is isomorphic holds
f is onto
let f be Function of S,T; :: thesis: ( f is isomorphic implies f is onto )
assume A1: f is isomorphic ; :: thesis: f is onto
per cases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; :: thesis: f is onto
hence rng f = the carrier of T by A1, WAYBEL_0:66; :: according to FUNCT_2:def 3 :: thesis: verum
end;
suppose ( S is empty or T is empty ) ; :: thesis: f is onto
then T is empty by A1, WAYBEL_0:def 38;
then the carrier of T = {} ;
hence rng f = the carrier of T ; :: according to FUNCT_2:def 3 :: thesis: verum
end;
end;