theorem Th3: :: LTLAXIO2:3

for f, g being FinSequence st rng f = rng g holds
( len f = 0 iff len g = 0 )