let m be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: ( n in dom f & m in dom ((f | n) /^ 1) implies ((f | n) /^ 1) . m = f . (m + 1) )

assume A0: n in dom f ; :: thesis: ( 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) ; :: thesis: ((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) ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: ( n in dom f & m in dom ((f | n) /^ 1) implies ((f | n) /^ 1) . m = f . (m + 1) )

assume A0: n in dom f ; :: thesis: ( 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) ; :: thesis: ((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) ; :: thesis: verum