theorem Th2: :: NUMERAL2:2

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