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

(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