reconsider f = Rascal 2 as 2 + 1 -element FinSequence ;
dom f = Seg (2 + 1) by Def1;
then ( 1 in dom f & 2 in dom f & 3 in dom f ) ;
then ( f . 1 = ((1 - 1) * ((2 + 1) - 1)) + 1 & f . 2 = ((2 - 1) * ((2 + 1) - 2)) + 1 & f . 3 = ((3 - 1) * ((2 + 1) - 3)) + 1 ) by Def1;
hence Rascal 2 = <*1,2,1*> ; :: thesis: verum