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 A1: f <> {} ; :: thesis: (f /. 1) .. f = 1
f " {(f /. 1)} c= dom f by RELAT_1:167;
then A2: f " {(f /. 1)} c= Seg (len f) by FINSEQ_1:def 3;
A3: 1 in dom f by A1, FINSEQ_5:6;
f /. 1 in {(f /. 1)} by TARSKI:def 1;
then A4: 1 in f " {(f /. 1)} by A3, PARTFUN2:44;
thus (f /. 1) .. f = (Sgm (f " {(f /. 1)})) . 1 by FINSEQ_4:def 5
.= 1 by A2, A4, Th3 ; :: thesis: verum