theorem Th40: :: FINSEQ_1:40

for p being FinSequence
for x being object holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )