let i be Nat; :: thesis: for df being FinSequence
for d being object st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i
let df be FinSequence; :: thesis: for d being object st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i
let d be object ; :: thesis: ( i in dom df implies (<*d*> ^ df) . (i + 1) = df . i )
A1: len (<*d*> ^ df) = (len <*d*>) + (len df) by FINSEQ_1:22
.= 1 + (len df) by FINSEQ_1:40 ;
assume A2: i in dom df ; :: thesis: (<*d*> ^ df) . (i + 1) = df . i
then i in Seg (len df) by FINSEQ_1:def 3;
then i + 1 in Seg (len (<*d*> ^ df)) by A1, FINSEQ_1:60;
then i + 1 in dom (<*d*> ^ df) by FINSEQ_1:def 3;
then A3: i + 1 <= len (<*d*> ^ df) by Th25;
A4: len <*d*> = 1 by FINSEQ_1:40;
1 <= i by A2, Th25;
then 1 < i + 1 by NAT_1:13;
hence (<*d*> ^ df) . (i + 1) = df . ((i + 1) - (len <*d*>)) by A4, A3, FINSEQ_1:24
.= df . i by A4 ;
:: thesis: verum