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 A1: ( 1 <= i & 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 A2: i -' 1 < i by A1, XREAL_1:235;
A3: len ((f | (i -' 1)) ^ <*p*>) = (len (f | (i -' 1))) + (len <*p*>) by FINSEQ_1:35
.= (i -' 1) + (len <*p*>) by A1, A2, FINSEQ_1:80, XXREAL_0:2
.= (i -' 1) + 1 by FINSEQ_1:56
.= i by A1, XREAL_1:237 ;
A4: len f = len (Replace f,i,p) by Th7
.= len (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) by A1, Def1
.= i + (len (f /^ i)) by A3, FINSEQ_1:35 ;
let k be Nat; :: thesis: ( 0 < k & k <= (len f) - i implies (Replace f,i,p) . (i + k) = (f /^ i) . k )
assume A5: ( 0 < k & k <= (len f) - i ) ; :: thesis: (Replace f,i,p) . (i + k) = (f /^ i) . k
then 0 + 1 <= k by INT_1:20;
then A6: k in dom (f /^ i) by A4, A5, FINSEQ_3:27;
(Replace f,i,p) . (i + k) = (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) . ((len ((f | (i -' 1)) ^ <*p*>)) + k) by A1, A3, Def1;
hence (Replace f,i,p) . (i + k) = (f /^ i) . k by A6, FINSEQ_1:def 7; :: thesis: verum