let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>
let D be non empty set ; :: thesis: for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>
let f be FinSequence of D; :: thesis: ( i + 1 = len f implies f = (f | i) ^ <*(f /. (len f))*> )
assume A1: i + 1 = len f ; :: thesis: f = (f | i) ^ <*(f /. (len f))*>
then not f is empty ;
then A2: i + 1 in dom f by A1, Th6;
dom f = Seg (i + 1) by A1, FINSEQ_1:def 3;
hence f = f | (Seg (i + 1))
.= (f | i) ^ <*(f . (i + 1))*> by A2, Th10
.= (f | i) ^ <*(f /. (len f))*> by A1, A2, PARTFUN1:def 6 ;
:: thesis: verum