theorem Th44: :: FINSEQ_1:44
for p being FinSequence
for x, y being object holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )