let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( 1 <= i & i <= len f & 1 <= j & j <= len f )
; :: thesis: Replace (Swap f,i,j),i,p = Swap (Replace f,j,p),i,j
then A2:
i in dom f
by FINSEQ_3:27;
per cases
( i = j or i < j or i > j )
by XXREAL_0:1;
suppose A3:
i = j
;
:: thesis: Replace (Swap f,i,j),i,p = Swap (Replace f,j,p),i,jthen
Replace (Swap f,i,j),
i,
p = Replace f,
i,
p
by Th21;
hence
Replace (Swap f,i,j),
i,
p = Swap (Replace f,j,p),
i,
j
by A3, Th21;
:: thesis: verum end; suppose A4:
i < j
;
:: thesis: Replace (Swap f,i,j),i,p = Swap (Replace f,j,p),i,jset F =
Swap f,
i,
j;
set M =
f | (i -' 1);
set N =
<*(f /. j)*>;
set P =
(f | (i -' 1)) ^ <*(f /. j)*>;
set Q =
((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j));
A5:
Swap f,
i,
j =
((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
by A1, A4, Th29
.=
(((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j))
by FINSEQ_1:45
.=
((f | (i -' 1)) ^ <*(f /. j)*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_1:45
;
A6:
i -' 1
<= i
by NAT_D:35;
A7:
len ((f | (i -' 1)) ^ <*(f /. j)*>) =
(len (f | (i -' 1))) + (len <*(f /. j)*>)
by FINSEQ_1:35
.=
(len (f | (i -' 1))) + 1
by FINSEQ_1:56
.=
(i -' 1) + 1
by A1, A6, FINSEQ_1:80, XXREAL_0:2
.=
i
by A1, XREAL_1:237
;
( 1
<= i &
i <= len (Swap f,i,j) & 1
<= j &
j <= len (Swap f,i,j) )
by A1, Th20;
then A8:
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 A7, Def1
.=
(((Swap f,i,j) | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by A5, FINSEQ_5:40
.=
((((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 A5, FINSEQ_1:45
.=
((((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 A1, A6, FINSEQ_1:80, XXREAL_0:2
.=
((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_5:26
;
set F1 =
Replace f,
j,
p;
set G1 =
f | (j -' 1);
set H1 =
<*p*>;
A9:
j -' 1
<= j
by NAT_D:35;
A10:
len ((f | (j -' 1)) ^ <*p*>) =
(len (f | (j -' 1))) + (len <*p*>)
by FINSEQ_1:35
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:56
.=
(j -' 1) + 1
by A1, A9, FINSEQ_1:80, XXREAL_0:2
.=
j
by A1, XREAL_1:237
;
A11:
i -' 1
< j -' 1
by A1, A4, NAT_D:56;
then A12:
i -' 1
<= len (f | (j -' 1))
by A1, A9, FINSEQ_1:80, XXREAL_0:2;
A13:
(Replace f,j,p) /^ j =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ j
by A1, Def1
.=
f /^ j
by A10, FINSEQ_5:40
;
A14:
(Replace f,j,p) | (i -' 1) =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (i -' 1)
by A1, Def1
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (i -' 1)
by FINSEQ_1:45
.=
(f | (j -' 1)) | (i -' 1)
by A12, FINSEQ_5:25
.=
f | (i -' 1)
by A11, FINSEQ_5:80
;
A15:
((Replace f,j,p) /^ i) | ((j -' i) -' 1) =
((Replace f,j,p) /^ i) | (j -' (i + 1))
by NAT_2:32
.=
((Replace f,j,p) /^ i) | ((j -' 1) -' i)
by NAT_2:32
.=
((Replace f,j,p) | (j -' 1)) /^ i
by FINSEQ_5:83
.=
((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1)) /^ i
by A1, Def1
.=
(((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1)) /^ i
by FINSEQ_1:45
.=
(((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1)))) /^ i
by A1, A9, FINSEQ_1:80, XXREAL_0:2
.=
(f | (j -' 1)) /^ i
by FINSEQ_5:26
.=
(f /^ i) | ((j -' 1) -' i)
by FINSEQ_5:83
.=
(f /^ i) | (j -' (1 + i))
by NAT_2:32
.=
(f /^ i) | ((j -' i) -' 1)
by NAT_2:32
;
A16:
( 1
<= i &
i <= len (Replace f,j,p) & 1
<= j &
j <= len (Replace f,j,p) )
by A1, Th7;
then A17:
i in dom (Replace f,j,p)
by FINSEQ_3:27;
A18:
j in dom (Replace f,j,p)
by A16, FINSEQ_3:27;
A19:
f . i =
(Replace f,j,p) . i
by A4, FUNCT_7:34
.=
(Replace f,j,p) /. i
by A17, PARTFUN1:def 8
;
A20:
p =
(Replace f,j,p) . j
by A1, Lm2
.=
(Replace f,j,p) /. j
by A18, PARTFUN1:def 8
;
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 A4, A16, Th29
.=
(((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f . i)*> ^ (f /^ j))
by A13, A14, A15, A19, A20, FINSEQ_1:45
.=
(((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f /. i)*> ^ (f /^ j))
by A2, PARTFUN1:def 8
.=
((f | (i -' 1)) ^ <*p*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f /. i)*> ^ (f /^ j)))
by FINSEQ_1:45
;
hence
Replace (Swap f,i,j),
i,
p = Swap (Replace f,j,p),
i,
j
by A8;
:: thesis: verum end; suppose A21:
i > j
;
:: thesis: Replace (Swap f,i,j),i,p = Swap (Replace f,j,p),i,jthen consider k being
Nat such that A22:
i = j + k
by NAT_1:10;
reconsider i =
i,
j =
j,
k =
k as
Element of
NAT by ORDINAL1:def 13;
A23:
i - j > j - j
by A21, XREAL_1:11;
then A24:
k = i -' j
by A22, XREAL_0:def 2;
A25:
i -' j <> 0
by A23, XREAL_0:def 2;
A26:
k >= 1
by A22, A23, NAT_1:14;
set F =
Swap f,
j,
i;
set M =
f | (j -' 1);
set N =
<*(f /. i)*>;
set P =
(f | (j -' 1)) ^ <*(f /. i)*>;
set V =
(f /^ j) | ((i -' j) -' 1);
set W =
<*(f /. j)*>;
set X =
f /^ i;
set Q =
(((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i);
A27:
Swap f,
j,
i =
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ i)
by A1, A21, Th29
.=
(((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ (<*(f /. j)*> ^ (f /^ i))
by FINSEQ_1:45
.=
((f | (j -' 1)) ^ <*(f /. i)*>) ^ (((f /^ j) | ((i -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ i)))
by FINSEQ_1:45
.=
((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))
by FINSEQ_1:45
;
A28:
j -' 1
<= j
by NAT_D:35;
A29:
len ((f | (j -' 1)) ^ <*(f /. i)*>) =
(len (f | (j -' 1))) + (len <*(f /. i)*>)
by FINSEQ_1:35
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:56
.=
(j -' 1) + 1
by A1, A28, FINSEQ_1:80, XXREAL_0:2
.=
j
by A1, XREAL_1:237
;
i -' 1
<= i
by NAT_D:35;
then
i -' 1
<= len f
by A1, XXREAL_0:2;
then
(i -' 1) -' j <= (len f) -' j
by NAT_D:42;
then
(i -' 1) -' j <= len (f /^ j)
by RFINSEQ:42;
then
i -' (1 + j) <= len (f /^ j)
by NAT_2:32;
then A30:
(i -' j) -' 1
<= len (f /^ j)
by NAT_2:32;
A31:
len (((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) =
(len ((f /^ j) | ((i -' j) -' 1))) + (len <*(f /. j)*>)
by FINSEQ_1:35
.=
(len ((f /^ j) | ((i -' j) -' 1))) + 1
by FINSEQ_1:56
.=
((i -' j) -' 1) + 1
by A30, FINSEQ_1:80
.=
i -' j
by A25, NAT_1:14, XREAL_1:237
;
A32:
j - 1
>= 1
- 1
by A1, XREAL_1:11;
A33:
(k + j) -' 1 =
(k + j) - 1
by A22, A23, NAT_1:14, NAT_D:37
.=
k + (j - 1)
.=
k + (j -' 1)
by A32, XREAL_0:def 2
;
A34:
k = 1
+ (k -' 1)
by A22, A23, NAT_1:14, XREAL_1:237;
A35:
len ((f /^ j) | ((i -' j) -' 1)) = k -' 1
by A24, A30, FINSEQ_1:80;
A36:
( 1
<= i &
i <= len (Swap f,j,i) & 1
<= j &
j <= len (Swap f,j,i) )
by A1, Th20;
A37:
Replace (Swap f,i,j),
i,
p =
Replace (Swap f,j,i),
i,
p
by Th23
.=
(((Swap f,j,i) | (i -' 1)) ^ <*p*>) ^ ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i))) /^ (j + k))
by A22, A27, A36, 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 A24, A29, A31, FINSEQ_5:39
.=
(((Swap f,j,i) | (k + (j -' 1))) ^ <*p*>) ^ (f /^ i)
by A22, A33, FINSEQ_5:40
.=
((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((j -' 1) + k)) ^ <*p*>) ^ (f /^ i)
by A27, FINSEQ_1:45
.=
((((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((((f /^ j) | ((i -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ i)))) | ((len (f | (j -' 1))) + k)) ^ <*p*>) ^ (f /^ i)
by A1, A28, FINSEQ_1:80, 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 A34, FINSEQ_1:56
.=
(((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:45
.=
(((f | (j -' 1)) ^ (<*(f /. i)*> ^ ((f /^ j) | ((i -' j) -' 1)))) ^ <*p*>) ^ (f /^ i)
by A35, FINSEQ_5:26
.=
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i)
by FINSEQ_1:45
;
set F1 =
Replace f,
j,
p;
set G1 =
f | (j -' 1);
set H1 =
<*p*>;
A38:
j -' 1
<= j
by NAT_D:35;
A39:
len ((f | (j -' 1)) ^ <*p*>) =
(len (f | (j -' 1))) + (len <*p*>)
by FINSEQ_1:35
.=
(len (f | (j -' 1))) + 1
by FINSEQ_1:56
.=
(j -' 1) + 1
by A1, A38, FINSEQ_1:80, XXREAL_0:2
.=
j
by A1, XREAL_1:237
;
then A40:
(Replace f,j,p) /^ i =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) /^ ((len ((f | (j -' 1)) ^ <*p*>)) + k)
by A1, A22, Def1
.=
(f /^ j) /^ k
by FINSEQ_5:39
.=
f /^ i
by A22, FINSEQ_6:87
;
A41:
k - 1
>= 1
- 1
by A26, XREAL_1:11;
A42:
(j + k) -' 1 =
(j + k) - 1
by A1, NAT_D:37
.=
j + (k - 1)
.=
j + (k -' 1)
by A41, XREAL_0:def 2
;
A43:
(Replace f,j,p) | (j -' 1) =
(((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j -' 1)
by A1, Def1
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (j -' 1)
by FINSEQ_1:45
.=
((f | (j -' 1)) ^ (<*p*> ^ (f /^ j))) | (len (f | (j -' 1)))
by A1, A38, FINSEQ_1:80, XXREAL_0:2
.=
f | (j -' 1)
by FINSEQ_5:26
;
A44:
((Replace f,j,p) /^ j) | ((i -' j) -' 1) =
((Replace f,j,p) /^ j) | (i -' (j + 1))
by NAT_2:32
.=
((Replace f,j,p) /^ j) | ((i -' 1) -' j)
by NAT_2:32
.=
((Replace f,j,p) | (i -' 1)) /^ j
by FINSEQ_5:83
.=
((((f | (j -' 1)) ^ <*p*>) ^ (f /^ j)) | (j + (k -' 1))) /^ j
by A1, A22, A42, Def1
.=
(((f | (j -' 1)) ^ <*p*>) ^ ((f /^ j) | (k -' 1))) /^ (len ((f | (j -' 1)) ^ <*p*>))
by A39, GENEALG1:2
.=
(f /^ j) | ((i -' j) -' 1)
by A24, FINSEQ_5:40
;
A45:
( 1
<= i &
i <= len (Replace f,j,p) & 1
<= j &
j <= len (Replace f,j,p) )
by A1, Th7;
then A46:
i in dom (Replace f,j,p)
by FINSEQ_3:27;
A47:
j in dom (Replace f,j,p)
by A45, FINSEQ_3:27;
A48:
f . i =
(Replace f,j,p) . i
by A21, FUNCT_7:34
.=
(Replace f,j,p) /. i
by A46, PARTFUN1:def 8
;
A49:
p =
(Replace f,j,p) . j
by A1, Lm2
.=
(Replace f,j,p) /. j
by A47, PARTFUN1:def 8
;
Swap (Replace f,j,p),
i,
j =
Swap (Replace f,j,p),
j,
i
by Th23
.=
(((((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 A21, A45, Th29
.=
((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*p*>) ^ (f /^ i)
by A2, A40, A43, A44, A48, A49, PARTFUN1:def 8
;
hence
Replace (Swap f,i,j),
i,
p = Swap (Replace f,j,p),
i,
j
by A37;
:: thesis: verum end;