consider A being set such that
A1: ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] ) by Def6;
s `2 in 2 -tuples_on A by A1, MCART_1:10;
then ex a, b being set st
( a in A & b in A & s `2 = <*a,b*> ) by Th10;
hence s `2 is FinSequence-like ; :: thesis: verum