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;