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

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