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