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