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