let m be Nat; for f being FinSequence of REAL
for n being Nat st n in dom f & m in dom ((f | n) /^ 1) holds
((f | n) /^ 1) . m = f . (m + 1)
let f be FinSequence of REAL ; for n being Nat st n in dom f & m in dom ((f | n) /^ 1) holds
((f | n) /^ 1) . m = f . (m + 1)
let n be Nat; ( n in dom f & m in dom ((f | n) /^ 1) implies ((f | n) /^ 1) . m = f . (m + 1) )
assume A0:
n in dom f
; ( not m in dom ((f | n) /^ 1) or ((f | n) /^ 1) . m = f . (m + 1) )
set F = f | n;
assume A1:
m in dom ((f | n) /^ 1)
; ((f | n) /^ 1) . m = f . (m + 1)
A1a:
m + 1 >= 0 + 1
by XREAL_1:6;
f | n <> {}
by A1;
then A2:
1 in dom (f | n)
by FINSEQ_5:6;
then
m + 1 <= len (f | n)
by A1, Th15, Th3;
then A4:
m + 1 <= n
by A0, Th10;
((f | n) /^ 1) . m =
((f | n) /^ 1) /. m
by A1, PARTFUN1:def 6
.=
(f | n) /. (1 + m)
by A1, FINSEQ_5:27
.=
(f | n) . (1 + m)
by A1, A2, Th15, PARTFUN1:def 6
.=
f . (1 + m)
by A0, Th7, A1a, A4
;
hence
((f | n) /^ 1) . m = f . (m + 1)
; verum