theorem Th2: :: LTLAXIO2:2

for n being Element of NAT
for f being FinSequence st len f = 0 holds
f /^ n = f