dom f = A
by FUNCT_2:def 1;

then dom (Re f) = A by COMSEQ_3:def 3;

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

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

then dom (Re f) = A by COMSEQ_3:def 3;

hence for b

b