let D be 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)
let f be 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)
let p, q be 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 i, j be Nat; ( 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 that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= len f
; Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)
set fp = f | (j -' 1);
A4:
j -' 1 <= j
by NAT_D:35;
1 + i <= j
by A2, INT_1:7;
then
i <= j -' 1
by NAT_D:55;
then A5:
i <= len (f | (j -' 1))
by A3, A4, FINSEQ_1:59, XXREAL_0:2;
set Q = f /^ j;
set F = Replace (f,j,q);
A6:
1 <= j
by A1, A2, XXREAL_0:2;
set fj = <*q*>;
set P = (f | (j -' 1)) ^ <*q*>;
A7: len ((f | (j -' 1)) ^ <*q*>) =
(len (f | (j -' 1))) + (len <*q*>)
by FINSEQ_1:22
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:39
.=
(j -' 1) + 1
by A3, A4, FINSEQ_1:59, XXREAL_0:2
.=
j
by A1, A2, XREAL_1:235, XXREAL_0:2
;
A8:
i -' 1 < j -' 1
by A1, A2, NAT_D:56;
then A9:
i -' 1 <= len (f | (j -' 1))
by A3, A4, FINSEQ_1:59, XXREAL_0:2;
i <= len f
by A2, A3, XXREAL_0:2;
then
i <= len (Replace (f,j,q))
by FUNCT_7:97;
then Replace ((Replace (f,j,q)),i,p) =
(((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((Replace (f,j,q)) /^ i)
by A1, Def1
.=
(((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) /^ i)
by A3, A6, Def1
.=
(((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*q*>) /^ i) ^ (f /^ j))
by A2, A7, GENEALG1:1
.=
(((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) /^ i) ^ <*q*>) ^ (f /^ j))
by A5, GENEALG1:1
.=
(((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((((f /^ i) | ((j -' 1) -' i)) ^ <*q*>) ^ (f /^ j))
by FINSEQ_5:80
.=
((((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' 1) -' i)) ^ <*q*>)) ^ (f /^ j)
by FINSEQ_1:32
.=
(((((Replace (f,j,q)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j)
by FINSEQ_1:32
.=
(((((((f | (j -' 1)) ^ <*q*>) ^ (f /^ j)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j)
by A3, A6, Def1
.=
((((((f | (j -' 1)) ^ <*q*>) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j)
by A2, A7, FINSEQ_5:22, NAT_D:44
.=
(((((f | (j -' 1)) | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j)
by A9, FINSEQ_5:22
.=
((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' 1) -' i))) ^ <*q*>) ^ (f /^ j)
by A8, FINSEQ_5:77
.=
((((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)
; verum