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