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