A1: dom (Rascal 0) = Seg (0 + 1) by Def1;
1 in dom (Rascal 0) by A1;
then (Rascal 0) . 1 = ((1 - 1) * ((0 + 1) - 1)) + 1 by Def1
.= <*1*> . 1 ;
hence Rascal 0 = <*1*> by A1, FINSEQ_1:def 8; :: thesis: verum