theorem Th11: :: FINSEQ_7:11

for D being non empty set
for f being FinSequence of D
for p, q being Element of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)