let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D holds (f | i) | i = f | i
let D be non empty set ; :: thesis: for f being FinSequence of D holds (f | i) | i = f | i
let f be FinSequence of D; :: thesis: (f | i) | i = f | i
f | i = f | (Seg i) by FINSEQ_1:def 15;
hence (f | i) | i = (f | (Seg i)) | (Seg i) by FINSEQ_1:def 15
.= f | ((Seg i) /\ (Seg i)) by RELAT_1:100
.= f | i by FINSEQ_1:def 15 ;
:: thesis: verum