theorem Th1: :: NUMERAL2:1

for f being non empty XFinSequence holds f | 1 = <%(f . 0)%>