dom (Rascal n) = Seg (n + 1) by Def1;
then A1: len (Rascal n) = n + 1 by FINSEQ_1:def 3;
(Rascal n) null n is len (Rascal n) -element ;
hence Rascal n is n + 1 -element by A1; :: thesis: verum