n in NAT by ORDINAL1:def 12;
then n in dom F by FUNCT_2:def 1;
then F . n in rng F by FUNCT_1:def 3;
hence F . n is PartFunc of D1,D2 ; :: thesis: verum