dom f = A
by FUNCT_2:def 1;

then dom (Im f) = A by COMSEQ_3:def 4;

hence for b_{1} being PartFunc of A,REAL st b_{1} = Im f holds

b_{1} is quasi_total
by FUNCT_2:def 1; :: thesis: verum

then dom (Im f) = A by COMSEQ_3:def 4;

hence for b

b