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

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