let D be non empty set ; :: thesis: for f being FinSequence of D
for q, p 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)
let f be FinSequence of D; :: thesis: for q, p 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)
let q, p be Element of D; :: thesis: 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)
let i, j be Nat; :: thesis: ( 1 <= i & i < j & j <= len f implies Replace (Replace f,j,q),i,p = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) )
assume A1: ( 1 <= i & i < j & j <= len f ) ; :: thesis: Replace (Replace f,j,q),i,p = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)
then A2: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) by XXREAL_0:2;
set F = Replace f,j,q;
A3: i <= len (Replace f,j,q) by A2, Th7;
set fp = f | (j -' 1);
set fj = <*q*>;
set P = (f | (j -' 1)) ^ <*q*>;
set Q = f /^ j;
A4: j -' 1 <= j by NAT_D:35;
A5: len ((f | (j -' 1)) ^ <*q*>) = (len (f | (j -' 1))) + (len <*q*>) by FINSEQ_1:35
.= (len (f | (j -' 1))) + 1 by FINSEQ_1:56
.= (j -' 1) + 1 by A1, A4, FINSEQ_1:80, XXREAL_0:2
.= j by A1, XREAL_1:237, XXREAL_0:2 ;
1 + i <= j by A1, INT_1:20;
then i <= j -' 1 by NAT_D:55;
then A6: i <= len (f | (j -' 1)) by A1, A4, FINSEQ_1:80, XXREAL_0:2;
A7: i -' 1 < j -' 1 by A1, NAT_D:56;
then A8: i -' 1 <= len (f | (j -' 1)) by A1, A4, FINSEQ_1:80, XXREAL_0:2;
Replace (Replace f,j,q),i,p = (((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((Replace f,j,q) /^ i) by A1, A3, Def1
.= (((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) /^ i) by A2, Def1
.= (((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) /^ i) ^ (f /^ j)) by A1, A5, GENEALG1:1
.= (((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) /^ i) ^ <*q*>) ^ (f /^ j)) by A6, GENEALG1:1
.= (((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((((f /^ i) | ((j -' 1) -' i)) ^ <*q*>) ^ (f /^ j)) by FINSEQ_5:83
.= ((((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' 1) -' i)) ^ <*q*>)) ^ (f /^ j) by FINSEQ_1:45
.= (((((Replace f,j,q) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by FINSEQ_1:45
.= (((((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A2, Def1
.= ((((((f | (j -' 1)) ^ <*q*>) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A1, A5, FINSEQ_5:25, NAT_D:44
.= (((((f | (j -' 1)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A8, FINSEQ_5:25
.= ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j) by A7, FINSEQ_5:80
.= ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) by Lm1 ;
hence Replace (Replace f,j,q),i,p = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j) ; :: thesis: verum