n < n + 1 by NAT_1:13;
then A1: ( X . (n + 1) = {} or X . n <> {} ) by Def2;
(FuncsSeq X) . n = Funcs ((X . (n + 1)),(X . n)) by Def3;
hence not (FuncsSeq X) . n is empty by A1, FUNCT_2:8; :: thesis: verum