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