let f be non empty XFinSequence; :: thesis: f | 1 = <%(f . 0)%>
A1: 0 in Segm (0 + 1) by NAT_1:45;
len f >= 1 by NAT_1:14;
then ( len (f | 1) = 1 & (f | 1) . 0 = f . 0 ) by AFINSQ_1:54, FUNCT_1:49, A1;
hence f | 1 = <%(f . 0)%> by AFINSQ_1:34; :: thesis: verum