theorem Th45: :: FINSEQ_1:45

for p being FinSequence
for x, y, z being object holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )