theorem Th35: :: AFINSQ_1:38

for x, y being object
for p being XFinSequence holds
( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )