theorem Th30: :: AFINSQ_1:33

for x being object
for p being XFinSequence holds
( p = <%x%> iff ( dom p = Segm 1 & rng p = {x} ) )