deffunc H₁( Element of F_Rat) -> Element of the carrier of F = ((canHom_Int F) . (numerator $1)) / ((canHom_Int F) . (denominator $1));
ex f being Function of F_Rat,F st
for x being Element of F_Rat holds f . x = H₁(x) from FUNCT_2:sch 4();
hence ex b₁ being Function of F_Rat,F st
for x being Element of F_Rat holds b₁ . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ; :: thesis: verum