A1: (FuncsSeq X) . n = Funcs (X . (n + 1)),(X . n) by Def5;

now

n < n + 1 by NAT_1:13;
hence ( X . (n + 1) = {} or X . n <> {} ) by Def4; :: thesis: verum

end;

hence not (FuncsSeq X) . n is empty by A1, FUNCT_2:11; :: thesis: verum