let D be set ; :: thesis: for f being FinSequence of D st not f is empty holds
f | 1 = <*(f /. 1)*>
let f be FinSequence of D; :: 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;
then 1 in dom (f | 1) by FINSEQ_3:25;
then ( (f | 1) /. 1 = (f | 1) . 1 & f /. 1 = (f | 1) /. 1 ) by FINSEQ_4:70, PARTFUN1:def 6;
hence f | 1 = <*(f /. 1)*> by A1, FINSEQ_1:40; :: thesis: verum