let f, g be Function of F_Rat,F; :: thesis: ( ( for x being Element of F_Rat holds f . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) & ( for x being Element of F_Rat holds g . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ) implies f = g )
assume that
A1: for x being Element of F_Rat holds f . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) and
A2: for x being Element of F_Rat holds g . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) ; :: thesis: f = g
let x be Element of F_Rat; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
thus f . x = ((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x)) by A1
.= g . x by A2 ; :: thesis: verum