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