n in NAT by ORDINAL1:def 13;
then n in dom F by FUNCT_2:def 1;
then A1: F . n in rng F by FUNCT_1:def 5;
thus F . n is PartFunc of D1,D2 by A1, PARTFUN1:120; :: thesis: verum