let i be natural number ; :: thesis: for df being FinSequence
for d being set st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i
let df be FinSequence; :: thesis: for d being set st i in dom df holds
(<*d*> ^ df) . (i + 1) = df . i
let d be set ; :: thesis: ( i in dom df implies (<*d*> ^ df) . (i + 1) = df . i )
assume A1: i in dom df ; :: thesis: (<*d*> ^ df) . (i + 1) = df . i
then A2: i in Seg (len df) by FINSEQ_1:def 3;
len (<*d*> ^ df) = (len <*d*>) + (len df) by FINSEQ_1:35
.= 1 + (len df) by FINSEQ_1:57 ;
then i + 1 in Seg (len (<*d*> ^ df)) by A2, FINSEQ_1:81;
then A3: i + 1 in dom (<*d*> ^ df) by FINSEQ_1:def 3;
A4: len <*d*> = 1 by FINSEQ_1:57;
1 <= i by A1, Th27;
then A5: 1 < i + 1 by NAT_1:13;
i + 1 <= len (<*d*> ^ df) by A3, Th27;
hence (<*d*> ^ df) . (i + 1) = df . ((i + 1) - (len <*d*>)) by A4, A5, FINSEQ_1:37
.= df . i by A4 ;
:: thesis: verum