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