theorem Th14: :: NUMBER11:14

for f being XFinSequence st len f >= 2 holds
f | 2 = <%(f . 0),(f . 1)%>