let x be set ; :: thesis: for k being Nat
for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
let k be Nat; :: thesis: for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
let p be FinSequence; :: thesis: ( k in dom p implies (<*x*> ^ p) . (k + 1) = p . k )
assume A1: k in dom p ; :: thesis: (<*x*> ^ p) . (k + 1) = p . k
k >= 1 by A1, FINSEQ_3:27;
then k >= len <*x*> by FINSEQ_1:56;
then A2: (len <*x*>) + 0 < k + 1 by XREAL_1:10;
(len <*x*>) + k in dom (<*x*> ^ p) by A1, FINSEQ_1:41;
then k + 1 in dom (<*x*> ^ p) by FINSEQ_1:56;
then k + 1 <= len (<*x*> ^ p) by FINSEQ_3:27;
then (<*x*> ^ p) . (k + 1) = p . ((k + 1) - (len <*x*>)) by A2, FINSEQ_1:37
.= p . ((k + 1) - 1) by FINSEQ_1:56
.= p . (k + (1 - 1)) ;
hence (<*x*> ^ p) . (k + 1) = p . k ; :: thesis: verum