theorem :: AFINSQ_1:15

for p being XFinSequence holds
( len p = 0 iff p = {} ) ;