theorem Th9: :: NAT_3:9

for f being FinSequence of REAL holds f |^ 0 = (len f) |-> 1