let D be non empty set ; :: thesis: for f being FinSequence of D st f <> {} holds
(f /. 1) .. f = 1
let f be FinSequence of D; :: thesis: ( f <> {} implies (f /. 1) .. f = 1 )
assume f <> {} ; :: thesis: (f /. 1) .. f = 1
then A1: 1 in dom f by FINSEQ_5:6;
f /. 1 in {(f /. 1)} by TARSKI:def 1;
then A2: 1 in f " {(f /. 1)} by A1, PARTFUN2:26;
f " {(f /. 1)} c= dom f by RELAT_1:132;
then A3: f " {(f /. 1)} c= Seg (len f) by FINSEQ_1:def 3;
thus (f /. 1) .. f = (Sgm (f " {(f /. 1)})) . 1 by FINSEQ_4:def 4
.= 1 by A3, A2, Th1 ; :: thesis: verum