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