reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
dom F = NAT by FIELD_12:def 2;
then A: F . n1 in rng F by FUNCT_1:3;
rng F c= Funcs (L1,L2) by RELAT_1:def 19;
then consider f being Function such that
B: ( f = F . n & dom f = the carrier of L1 & rng f c= the carrier of L2 ) by A, FUNCT_2:def 2;
thus F . n is Function of L1,L2 by B, FUNCT_2:2; :: thesis: verum