let X be non empty set ; :: thesis: for t being FinSequence of X
for k being Nat st k + 1 <= len t holds
t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1))
let t be FinSequence of X; :: thesis: for k being Nat st k + 1 <= len t holds
t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1))
let k be Nat; :: thesis: ( k + 1 <= len t implies t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1)) )
A1: (k + 1) -' 1 = (k + 1) - 1 by XREAL_0:def 2
.= k ;
assume k + 1 <= len t ; :: thesis: t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1))
then t = ((t | ((k + 1) -' 1)) ^ <*(t . (k + 1))*>) ^ (t /^ (k + 1)) by NAT_1:11, FINSEQ_5:84
.= (t | k) ^ (<*(t . (k + 1))*> ^ (t /^ (k + 1))) by A1, FINSEQ_1:32 ;
then (t | k) ^ (t /^ k) = (t | k) ^ (<*(t . (k + 1))*> ^ (t /^ (k + 1))) by RFINSEQ:8;
hence t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1)) by FINSEQ_1:33; :: thesis: verum