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