let p be FinSequence; :: thesis: ( len p <> 0 implies p | 1 = <*(p . 1)*> )
assume len p <> 0 ; :: thesis: p | 1 = <*(p . 1)*>
then A1: len (p | 1) = 1 by NAT_1:14, FINSEQ_1:59;
then 1 in dom (p | 1) by FINSEQ_3:25;
then A2: 1 in dom (p | (Seg 1)) by FINSEQ_1:def 16;
(p | 1) . 1 = (p | (Seg 1)) . 1 by FINSEQ_1:def 16
.= p . 1 by A2, FUNCT_1:47 ;
hence p | 1 = <*(p . 1)*> by A1, FINSEQ_1:40; :: thesis: verum