let f be FinSequence; :: thesis: ( not f is empty implies f | 1 = <*(f . 1)*> )
assume not f is empty ; :: thesis: f | 1 = <*(f . 1)*>
then 1 in dom f by Th6;
then 1 <= len f by FINSEQ_3:25;
then A1: len (f | 1) = 1 by FINSEQ_1:59;
(f | (Seg 1)) . 1 = f . 1 by FINSEQ_1:1, FUNCT_1:49;
hence f | 1 = <*(f . 1)*> by A1, FINSEQ_1:40; :: thesis: verum