theorem Th38: :: FINSEQ_1:38

for p being FinSequence
for x being object holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )