let D be non empty set ; for f being FinSequence of D
for p being Element of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)
let f be FinSequence of D; for p being Element of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)
let p be Element of D; for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)
let i, j be Nat; ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j) )
assume that
A1:
1 <= i
and
A2:
i <= len f
and
A3:
1 <= j
and
A4:
j <= len f
; Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)
A5:
i in dom f
by A1, A2, FINSEQ_3:25;
per cases
( i = j or i < j or i > j )
by XXREAL_0:1;
suppose A6:
i = j
;
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)then
Replace (
(Swap (f,i,j)),
i,
p)
= Replace (
f,
i,
p)
by Th19;
hence
Replace (
(Swap (f,i,j)),
i,
p)
= Swap (
(Replace (f,j,p)),
i,
j)
by A6, Th19;
verum end; suppose A7:
i < j
;
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)set N =
<*(f /. j)*>;
set M =
f | (i -' 1);
set F =
Swap (
f,
i,
j);
set P =
(f | (i -' 1)) ^ <*(f /. j)*>;
A8:
Swap (
f,
i,
j) =
((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
by A1, A4, A7, Th27
.=
(((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j))
by FINSEQ_1:32
.=
((f | (i -' 1)) ^ <*(f /. j)*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_1:32
;
set F1 =
Replace (
f,
j,
p);
i <= len (Replace (f,j,p))
by A2, FUNCT_7:97;
then A9:
i in dom (Replace (f,j,p))
by A1, FINSEQ_3:25;
A10:
f . i =
(Replace (f,j,p)) . i
by A7, FUNCT_7:32
.=
(Replace (f,j,p)) /. i
by A9, PARTFUN1:def 6
;
A11:
j <= len (Replace (f,j,p))
by A4, FUNCT_7:97;
then A12:
j in dom (Replace (f,j,p))
by A3, FINSEQ_3:25;
set G1 =
f | (j -' 1);
A13:
j -' 1
<= j
by NAT_D:35;
A14:
i -' 1
< j -' 1
by A1, A7, NAT_D:56;
then A15:
i -' 1
<= len (f | (j -' 1))
by A4, A13, FINSEQ_1:59, XXREAL_0:2;
set H1 =
<*p*>;
set Q =
((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j));
A16:
i -' 1
<= i
by NAT_D:35;
A17:
i <= len (Swap (f,i,j))
by A2, Th18;
len ((f | (i -' 1)) ^ <*(f /. j)*>) =
(len (f | (i -' 1))) + (len <*(f /. j)*>)
by FINSEQ_1:22
.=
(len (f | (i -' 1))) + 1
by FINSEQ_1:39
.=
(i -' 1) + 1
by A2, A16, FINSEQ_1:59, XXREAL_0:2
.=
i
by A1, XREAL_1:235
;
then A18:
Replace (
(Swap (f,i,j)),
i,
p) =
(((Swap (f,i,j)) | (i -' 1)) ^ <*p*>) ^ ((Swap (f,i,j)) /^ (len ((f | (i -' 1)) ^ <*(f /. j)*>)))
by A1, A17, Def1
.=
(((Swap (f,i,j)) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by A8, FINSEQ_5:37
.=
((((f | (i -' 1)) ^ (<*(f /. j)*> ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))))) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by A8, FINSEQ_1:32
.=
((((f | (i -' 1)) ^ (<*(f /. j)*> ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j))))) | (len (f | (i -' 1)))) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by A2, A16, FINSEQ_1:59, XXREAL_0:2
.=
((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_5:23
;
A19:
len ((f | (j -' 1)) ^ <*p*>) =
(len (f | (j -' 1))) + (len <*p*>)
by FINSEQ_1:22
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:39
.=
(j -' 1) + 1
by A4, A13, FINSEQ_1:59, XXREAL_0:2
.=
j
by A3, XREAL_1:235
;
A20:
((Replace (f,j,p)) /^ i) | ((j -' i) -' 1) =
((Replace (f,j,p)) /^ i) | (j -' (i + 1))
by NAT_2:30
.=
((Replace (f,j,p)) /^ i) | ((j -' 1) -' i)
by NAT_2:30
.=
((Replace (f,j,p)) | (j -' 1)) /^ i
by FINSEQ_5:80
.=
((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1)) /^ i
by A3, A4, Def1
.=
(((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1)) /^ i
by FINSEQ_1:32
.=
(((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1)))) /^ i
by A4, A13, FINSEQ_1:59, XXREAL_0:2
.=
(f | (j -' 1)) /^ i
by FINSEQ_5:23
.=
(f /^ i) | ((j -' 1) -' i)
by FINSEQ_5:80
.=
(f /^ i) | (j -' (1 + i))
by NAT_2:30
.=
(f /^ i) | ((j -' i) -' 1)
by NAT_2:30
;
A21:
p =
(Replace (f,j,p)) . j
by A3, A4, Lm2
.=
(Replace (f,j,p)) /. j
by A12, PARTFUN1:def 6
;
A22:
(Replace (f,j,p)) | (i -' 1) =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (i -' 1)
by A3, A4, Def1
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (i -' 1)
by FINSEQ_1:32
.=
(f | (j -' 1)) | (i -' 1)
by A15, FINSEQ_5:22
.=
f | (i -' 1)
by A14, FINSEQ_5:77
;
A23:
(Replace (f,j,p)) /^ j =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ j
by A3, A4, Def1
.=
f /^ j
by A19, FINSEQ_5:37
;
Swap (
(Replace (f,j,p)),
i,
j) =
(((((Replace (f,j,p)) | (i -' 1)) ^ <*((Replace (f,j,p)) /. j)*>) ^ (((Replace (f,j,p)) /^ i) | ((j -' i) -' 1))) ^ <*((Replace (f,j,p)) /. i)*>) ^ ((Replace (f,j,p)) /^ j)
by A1, A7, A11, Th27
.=
(((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f . i)*> ^ (f /^ j))
by A23, A22, A20, A10, A21, FINSEQ_1:32
.=
(((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j))
by A5, PARTFUN1:def 6
.=
((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_1:32
;
hence
Replace (
(Swap (f,i,j)),
i,
p)
= Swap (
(Replace (f,j,p)),
i,
j)
by A18;
verum end; suppose A24:
i > j
;
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)then consider k being
Nat such that A25:
i = j + k
by NAT_1:10;
reconsider i =
i,
j =
j,
k =
k as
Element of
NAT by ORDINAL1:def 12;
A26:
i - j > j - j
by A24, XREAL_1:9;
then A27:
k = i -' j
by A25, XREAL_0:def 2;
set X =
f /^ i;
set W =
<*(f /. j)*>;
set V =
(f /^ j) | ((i -' j) -' 1);
set N =
<*(f /. i)*>;
set M =
f | (j -' 1);
set F =
Swap (
f,
j,
i);
set P =
(f | (j -' 1)) ^ <*(f /. i)*>;
A28:
Swap (
f,
j,
i) =
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ i)
by A2, A3, A24, Th27
.=
(((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ (<*(f /. j)*> ^ (f /^ i))
by FINSEQ_1:32
.=
((f | (j -' 1)) ^ <*(f /. i)*>) ^ (((f /^ j) | ((i -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ i)))
by FINSEQ_1:32
.=
((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))
by FINSEQ_1:32
;
A29:
j - 1
>= 1
- 1
by A3, XREAL_1:9;
A30:
(k + j) -' 1 =
(k + j) - 1
by A25, A26, NAT_1:14, NAT_D:37
.=
k + (j - 1)
.=
k + (j -' 1)
by A29, XREAL_0:def 2
;
A31:
k = 1
+ (k -' 1)
by A25, A26, NAT_1:14, XREAL_1:235;
set Q =
(((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i);
A32:
j -' 1
<= j
by NAT_D:35;
set F1 =
Replace (
f,
j,
p);
set G1 =
f | (j -' 1);
A33:
j -' 1
<= j
by NAT_D:35;
set H1 =
<*p*>;
j <= len (Replace (f,j,p))
by A4, FUNCT_7:97;
then A34:
j in dom (Replace (f,j,p))
by A3, FINSEQ_3:25;
A35:
len ((f | (j -' 1)) ^ <*p*>) =
(len (f | (j -' 1))) + (len <*p*>)
by FINSEQ_1:22
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:39
.=
(j -' 1) + 1
by A4, A33, FINSEQ_1:59, XXREAL_0:2
.=
j
by A3, XREAL_1:235
;
then A36:
(Replace (f,j,p)) /^ i =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ ((len ((f | (j -' 1)) ^ <*p*>)) + k)
by A3, A4, A25, Def1
.=
(f /^ j) /^ k
by FINSEQ_5:36
.=
f /^ i
by A25, FINSEQ_6:81
;
k >= 1
by A25, A26, NAT_1:14;
then A37:
k - 1
>= 1
- 1
by XREAL_1:9;
A38:
(j + k) -' 1 =
(j + k) - 1
by A3, NAT_D:37
.=
j + (k - 1)
.=
j + (k -' 1)
by A37, XREAL_0:def 2
;
A39:
i <= len (Replace (f,j,p))
by A2, FUNCT_7:97;
then A40:
i in dom (Replace (f,j,p))
by A1, FINSEQ_3:25;
A41:
((Replace (f,j,p)) /^ j) | ((i -' j) -' 1) =
((Replace (f,j,p)) /^ j) | (i -' (j + 1))
by NAT_2:30
.=
((Replace (f,j,p)) /^ j) | ((i -' 1) -' j)
by NAT_2:30
.=
((Replace (f,j,p)) | (i -' 1)) /^ j
by FINSEQ_5:80
.=
((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j + (k -' 1))) /^ j
by A3, A4, A25, A38, Def1
.=
(((f | (j -' 1)) ^ <*p*>) ^ ((f /^ j) | (k -' 1))) /^ (len ((f | (j -' 1)) ^ <*p*>))
by A35, GENEALG1:2
.=
(f /^ j) | ((i -' j) -' 1)
by A27, FINSEQ_5:37
;
A42:
(Replace (f,j,p)) | (j -' 1) =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1)
by A3, A4, Def1
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1)
by FINSEQ_1:32
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1)))
by A4, A33, FINSEQ_1:59, XXREAL_0:2
.=
f | (j -' 1)
by FINSEQ_5:23
;
A43:
p =
(Replace (f,j,p)) . j
by A3, A4, Lm2
.=
(Replace (f,j,p)) /. j
by A34, PARTFUN1:def 6
;
A44:
f . i =
(Replace (f,j,p)) . i
by A24, FUNCT_7:32
.=
(Replace (f,j,p)) /. i
by A40, PARTFUN1:def 6
;
A45:
Swap (
(Replace (f,j,p)),
i,
j) =
Swap (
(Replace (f,j,p)),
j,
i)
by Th21
.=
(((((Replace (f,j,p)) | (j -' 1)) ^ <*((Replace (f,j,p)) /. i)*>) ^ (((Replace (f,j,p)) /^ j) | ((i -' j) -' 1))) ^ <*((Replace (f,j,p)) /. j)*>) ^ ((Replace (f,j,p)) /^ i)
by A3, A24, A39, Th27
.=
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i)
by A5, A36, A42, A41, A44, A43, PARTFUN1:def 6
;
A46:
i -' j <> 0
by A26, XREAL_0:def 2;
i -' 1
<= i
by NAT_D:35;
then
i -' 1
<= len f
by A2, XXREAL_0:2;
then
(i -' 1) -' j <= (len f) -' j
by NAT_D:42;
then
(i -' 1) -' j <= len (f /^ j)
by RFINSEQ:29;
then
i -' (1 + j) <= len (f /^ j)
by NAT_2:30;
then A47:
(i -' j) -' 1
<= len (f /^ j)
by NAT_2:30;
then A48:
len ((f /^ j) | ((i -' j) -' 1)) = k -' 1
by A27, FINSEQ_1:59;
A49:
len ((f | (j -' 1)) ^ <*(f /. i)*>) =
(len (f | (j -' 1))) + (len <*(f /. i)*>)
by FINSEQ_1:22
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:39
.=
(j -' 1) + 1
by A4, A32, FINSEQ_1:59, XXREAL_0:2
.=
j
by A3, XREAL_1:235
;
A50:
i <= len (Swap (f,j,i))
by A2, Th18;
A51:
len (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) =
(len ((f /^ j) | ((i -' j) -' 1))) + (len <*(f /. j)*>)
by FINSEQ_1:22
.=
(len ((f /^ j) | ((i -' j) -' 1))) + 1
by FINSEQ_1:39
.=
((i -' j) -' 1) + 1
by A47, FINSEQ_1:59
.=
i -' j
by A46, NAT_1:14, XREAL_1:235
;
Replace (
(Swap (f,i,j)),
i,
p) =
Replace (
(Swap (f,j,i)),
i,
p)
by Th21
.=
(((Swap (f,j,i)) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) /^ (j + k))
by A1, A25, A28, A50, Def1
.=
(((Swap (f,j,i)) | (i -' 1)) ^ <*p*>) ^ (((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)) /^ (len (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>)))
by A27, A49, A51, FINSEQ_5:36
.=
(((Swap (f,j,i)) | (k + (j -' 1))) ^ <*p*>) ^ (f /^ i)
by A25, A30, FINSEQ_5:37
.=
((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((j -' 1) + k)) ^ <*p*>) ^ (f /^ i)
by A28, FINSEQ_1:32
.=
((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((len (f | (j -' 1))) + k)) ^ <*p*>) ^ (f /^ i)
by A4, A32, FINSEQ_1:59, XXREAL_0:2
.=
(((f | (j -' 1)) ^ ((<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) | k)) ^ <*p*>) ^ (f /^ i)
by GENEALG1:2
.=
(((f | (j -' 1)) ^ ((<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) | ((len <*(f /. i)*>) + (k -' 1)))) ^ <*p*>) ^ (f /^ i)
by A31, FINSEQ_1:39
.=
(((f | (j -' 1)) ^ (<*(f /. i)*> ^ (((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)) | (k -' 1)))) ^ <*p*>) ^ (f /^ i)
by GENEALG1:2
.=
(((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ i))) | (k -' 1)))) ^ <*p*>) ^ (f /^ i)
by FINSEQ_1:32
.=
(((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((f /^ j) | ((i -' j) -' 1)))) ^ <*p*>) ^ (f /^ i)
by A48, FINSEQ_5:23
.=
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i)
by FINSEQ_1:32
;
hence
Replace (
(Swap (f,i,j)),
i,
p)
= Swap (
(Replace (f,j,p)),
i,
j)
by A45;
verum end;