let f be Homomorphism of F_Rat,F_Rat; :: thesis: f = id F_Rat
id F_Rat = canHom_Rat F_Rat by Th98;
hence f = id F_Rat by Th98; :: thesis: verum