set f = canHom_Rat F;
set c = canHom_Int F;
A1: ( numerator 1 = 1 & denominator 1 = 1 ) by RAT_1:17;
(canHom_Int F) . (1_ INT.Ring) = 1_ F by GROUP_1:def 13;
hence (canHom_Rat F) . (1_ F_Rat) = (1. F) / (1. F) by A1, Def11
.= 1_ F ;
:: according to GROUP_1:def 13 :: thesis: verum