let f, g be Function of RAT,NAT; :: thesis: ( ( for x being Rational holds f . x = denominator x ) & ( for x being Rational holds g . x = denominator x ) implies f = g )
assume that
A3: for x being Rational holds f . x = denominator x and
A4: for x being Rational holds g . x = denominator x ; :: thesis: f = g

now :: thesis: for x being Element of RAT holds f . x = g . x

let x be Element of RAT ; :: thesis: f . x = g . x
f . x = denominator x by A3;
hence f . x = g . x by A4; :: thesis: verum

end;

hence f = g ; :: thesis: verum