let n be Nat; :: thesis: (Rascal n) . 1 = 1
reconsider f = Rascal n as n + 1 -element FinSequence ;
A1: dom f = Seg (n + 1) by Def1;
1 + 0 <= 1 + n by XREAL_1:6;
then 1 in dom f by A1;
then f . 1 = ((1 - 1) * ((n + 1) - 1)) + 1 by Def1;
hence (Rascal n) . 1 = 1 ; :: thesis: verum