dom f = A by FUNCT_2:def 1;
then dom (Im f) = A by COMSEQ_3:def 4;
hence for b₁ being PartFunc of A,REAL st b₁ = Im f holds
b₁ is quasi_total by FUNCT_2:def 1; :: thesis: verum