let f be XFinSequence; :: thesis: ( len f >= 2 implies f | 2 = <%(f . 0),(f . 1)%> )
assume A1: len f >= 2 ; :: thesis: f | 2 = <%(f . 0),(f . 1)%>
then A2: len (f | 2) = 2 by AFINSQ_1:54;
0 in Segm 2 by NAT_1:44;
then A3: (f | 2) . 0 = f . 0 by A1, AFINSQ_1:53;
1 in Segm 2 by NAT_1:44;
then A4: (f | 2) . 1 = f . 1 by A1, AFINSQ_1:53;
thus f | 2 = <%(f . 0),(f . 1)%> by AFINSQ_1:38, A2, A3, A4; :: thesis: verum