theorem Th31: :: AFINSQ_1:34

for x being object
for p being XFinSequence holds
( p = <%x%> iff ( len p = 1 & p . 0 = x ) ) by Def4;