let D be non empty set ; for f being FinSequence of D st f <> {} holds
(f /. 1) .. f = 1
let f be FinSequence of D; ( f <> {} implies (f /. 1) .. f = 1 )
assume
f <> {}
; (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
f " {(f /. 1)} c= Seg (len f)
by FINSEQ_1:def 3;
then A3:
f " {(f /. 1)} is included_in_Seg
;
thus (f /. 1) .. f =
(Sgm (f " {(f /. 1)})) . 1
by FINSEQ_4:def 4
.=
1
by A3, A2, Th1
; verum