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

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