let f be FinSequence; :: thesis: ( 1 <= len f implies f | (Seg 1) = <*(f . 1)*> )
assume 1 <= len f ; :: thesis: f | (Seg 1) = <*(f . 1)*>
then Seg 1 c= Seg (len f) by FINSEQ_1:5;
then A1: Seg 1 c= dom f by FINSEQ_1:def 3;
reconsider f1 = f | (Seg 1) as FinSequence by FINSEQ_1:15;
0 + 1 in Seg 1 by FINSEQ_1:4;
then A2: (f | (Seg 1)) . 1 = f . 1 by FUNCT_1:49;
dom f1 = Seg 1 by A1, RELAT_1:62;
then len f1 = 1 by FINSEQ_1:def 3;
hence f | (Seg 1) = <*(f . 1)*> by A2, FINSEQ_1:40; :: thesis: verum