let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k
let f be FinSequence of D; :: thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k
let p be Element of D; :: thesis: for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k )
assume that
A1: 1 <= i and
A2: i <= len f ; :: thesis: for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k
i - 1 < i by XREAL_1:148;
then A3: i -' 1 < i by A1, XREAL_1:235;
A4: len ((f | (i -' 1)) ^ <*p*>) = (len (f | (i -' 1))) + (len <*p*>) by FINSEQ_1:35
.= (i -' 1) + (len <*p*>) by A2, A3, FINSEQ_1:80, XXREAL_0:2
.= (i -' 1) + 1 by FINSEQ_1:56
.= i by A1, XREAL_1:237 ;
let k be Nat; :: thesis: ( 0 < k & k <= (len f) - i implies (Replace f,i,p) . (i + k) = (f /^ i) . k )
assume that
A5: 0 < k and
A6: k <= (len f) - i ; :: thesis: (Replace f,i,p) . (i + k) = (f /^ i) . k
A7: 0 + 1 <= k by A5, INT_1:20;
len f = len (Replace f,i,p) by Th7
.= len (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) by A1, A2, Def1
.= i + (len (f /^ i)) by A4, FINSEQ_1:35 ;
then A8: k in dom (f /^ i) by A6, A7, FINSEQ_3:27;
(Replace f,i,p) . (i + k) = (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) . ((len ((f | (i -' 1)) ^ <*p*>)) + k) by A1, A2, A4, Def1;
hence (Replace f,i,p) . (i + k) = (f /^ i) . k by A8, FINSEQ_1:def 7; :: thesis: verum