n <= n + 1 by NAT_1:11;
then A1: Seg n c= Seg (n + 1) by FINSEQ_1:5;
A2: rng (id (Seg n)) = Seg n ;
dom (id (Seg n)) = Seg n ;
then reconsider n1 = idseq n as Element of Funcs ((Seg n),(Seg (n + 1))) by A1, A2, FUNCT_2:def 2;
@ n1 is increasing ;
then n1 in { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ;
hence not NatEmbSeq . n is empty by Def5; :: thesis: verum