reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then A1: f . n in rng f by FUNCT_1:def 3;
rng f c= [:D,RAT:] by RELAT_1:def 19;
then (f . n) `2 in RAT by A1, MCART_1:10;
hence (f . n) `2 is rational ; :: thesis: verum