let f be FinSequence; :: thesis: ( 1 <= len f implies f | (Seg 1) = <*(f . 1)*> )
assume A1: 1 <= len f ; :: thesis: f | (Seg 1) = <*(f . 1)*>
reconsider f1 = f | (Seg 1) as FinSequence by FINSEQ_1:19;
Seg 1 c= Seg (len f) by A1, FINSEQ_1:7;
then Seg 1 c= dom f by FINSEQ_1:def 3;
then dom f1 = Seg 1 by RELAT_1:91;
then A2: len f1 = 1 by FINSEQ_1:def 3;
0 + 1 in Seg 1 by FINSEQ_1:6;
then (f | (Seg 1)) . 1 = f . 1 by FUNCT_1:72;
hence f | (Seg 1) = <*(f . 1)*> by A2, FINSEQ_1:57; :: thesis: verum