:: FINSEQ_7 semantic presentation

begin


theorem :: FINSEQ_7:1
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & j <= len f & i < j holds
f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat st 1 <= i & j <= len f & i < j holds
f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & j <= len f & i < j holds
f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
let i, j be Nat; ::_thesis: ( 1 <= i & j <= len f & i < j implies f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) )
assume that
A1: 1 <= i and
A2: j <= len f and
A3: i < j ; ::_thesis: f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
A4: i <= len f by A2, A3, XXREAL_0:2;
 1 <= j by A1, A3, XXREAL_0:2;
then A5: j in dom f by A2, FINSEQ_3:25;
set I = (j -' i) -' 1;
 i -' i < j -' i by A3, NAT_D:57;
then A6: ((j -' i) -' 1) + 1 = j -' i by NAT_1:14, XREAL_1:235;
 j -' i <= (len f) -' i by A2, NAT_D:42;
then A7: ((j -' i) -' 1) + 1 <= len (f /^ i) by A6, RFINSEQ:29;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
A8: i < len (f | j) by A2, A3, FINSEQ_1:59;
 1 <= ((j -' i) -' 1) + 1 by NAT_1:14;
then A9: ((j -' i) -' 1) + 1 in dom (f /^ i) by A7, FINSEQ_3:25;
 (((j -' i) -' 1) + 1) + i = j by A3, A6, XREAL_1:235;
then A10: (f /^ i) /. (((j -' i) -' 1) + 1) = f /. j by A9, FINSEQ_5:27;
A11: f /^ i = ((f | j) ^ (f /^ j)) /^ i by RFINSEQ:8
.= ((f | j) /^ i) ^ (f /^ j) by A8, GENEALG1:1
.= ((f /^ i) | (((j -' i) -' 1) + 1)) ^ (f /^ j) by A6, FINSEQ_5:80
.= (((f /^ i) | ((j -' i) -' 1)) ^ <*((f /^ i) /. (((j -' i) -' 1) + 1))*>) ^ (f /^ j) by A7, FINSEQ_5:82
.= (((f /^ i) | ((j -' i) -' 1)) ^ <*(f . j)*>) ^ (f /^ j) by A5, A10, PARTFUN1:def_6 ;
f = ((f | (i -' 1)) ^ <*(f . i)*>) ^ (f /^ i) by A1, A4, FINSEQ_5:84
.= ((f | (i -' 1)) ^ <*(f . i)*>) ^ (((f /^ i) | ((j -' i) -' 1)) ^ (<*(f . j)*> ^ (f /^ j))) by A11, FINSEQ_1:32
.= (((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ (<*(f . j)*> ^ (f /^ j)) by FINSEQ_1:32
.= ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) by FINSEQ_1:32 ;
hence  f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j) ; ::_thesis: verum
end;

theorem :: FINSEQ_7:2
for i being Nat
for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds
(g ^ f) . i = (h ^ f) . i
proof
let i be Nat; ::_thesis: for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds
(g ^ f) . i = (h ^ f) . i
let f, g, h be FinSequence; ::_thesis: ( len g = len h & len g < i & i <= len (g ^ f) implies (g ^ f) . i = (h ^ f) . i )
assume that
A1: len g = len h and
A2: len g < i and
A3: i <= len (g ^ f) ; ::_thesis: (g ^ f) . i = (h ^ f) . i
 i <= (len g) + (len f) by A3, FINSEQ_1:22;
then A4: i - (len g) <= ((len g) + (len f)) - (len g) by XREAL_1:9;
set k = i - (len g);
A5: (len g) - (len g) < i - (len g) by A2, XREAL_1:9;
then reconsider k = i - (len g) as Element of NAT by INT_1:3;
 0 + 1 <= i - (len g) by A5, INT_1:7;
then A6: k in dom f by A4, FINSEQ_3:25;
(g ^ f) . i = (g ^ f) . (k + (len g))
.= f . k by A6, FINSEQ_1:def_7
.= (h ^ f) . ((len h) + k) by A6, FINSEQ_1:def_7 ;
hence  (g ^ f) . i = (h ^ f) . i by A1; ::_thesis: verum
end;

theorem :: FINSEQ_7:3
for i being Nat
for f, g being FinSequence st 1 <= i & i <= len f holds
f . i = (g ^ f) . ((len g) + i)
proof
let i be Nat; ::_thesis: for f, g being FinSequence st 1 <= i & i <= len f holds
f . i = (g ^ f) . ((len g) + i)
let f, g be FinSequence; ::_thesis: ( 1 <= i & i <= len f implies f . i = (g ^ f) . ((len g) + i) )
assume  ( 1 <= i & i <= len f ) ; ::_thesis: f . i = (g ^ f) . ((len g) + i)
then  i in dom f by FINSEQ_3:25;
hence  f . i = (g ^ f) . ((len g) + i) by FINSEQ_1:def_7; ::_thesis: verum
end;

theorem :: FINSEQ_7:4
for D being non empty set
for f being FinSequence of D
for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
let f be FinSequence of D; ::_thesis: for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
let i, n be Nat; ::_thesis: ( i in dom (f /^ n) implies (f /^ n) . i = f . (n + i) )
assume A1: i in dom (f /^ n) ; ::_thesis: (f /^ n) . i = f . (n + i)
reconsider i = i, n = n as Element of NAT by ORDINAL1:def_12;
A2: n + i in dom f by A1, FINSEQ_5:26;
 ( (f /^ n) /. i = f /. (n + i) & (f /^ n) /. i = (f /^ n) . i ) by A1, FINSEQ_5:27, PARTFUN1:def_6;
hence  (f /^ n) . i = f . (n + i) by A2, PARTFUN1:def_6; ::_thesis: verum
end;

Lm1:  for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i
proof
let j, i be Nat; ::_thesis: (j -' i) -' 1 = (j -' 1) -' i
 (j -' i) -' 1 = j -' (i + 1) by NAT_2:30;
hence  (j -' i) -' 1 = (j -' 1) -' i by NAT_2:30; ::_thesis: verum
end;

begin

notation
let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
synonym  Replace (f,i,p) for D +* (f,i);
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
:: original: Replace
redefine func Replace (f,i,p) ->  FinSequence of D equals :Def1: :: FINSEQ_7:def 1
((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f )
otherwise f;
compatibility
 for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b1 = Replace (i,p,) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (i,p,) iff b1 = f ) ) )
proof
A1: ( ( not 1 <= i or not i <= len f ) implies f +* (i,p) = f )
proof
assume  ( not 1 <= i or not i <= len f ) ; ::_thesis: f +* (i,p) = f
then  not i in dom f by FINSEQ_3:25;
hence  f +* (i,p) = f by FUNCT_7:def_3; ::_thesis: verum
end;
 ( 1 <= i & i <= len f implies f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) )
proof
assume  ( 1 <= i & i <= len f ) ; ::_thesis: f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)
then  i in dom f by FINSEQ_3:25;
hence  f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) by FUNCT_7:98; ::_thesis: verum
end;
hence  for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b1 = Replace (i,p,) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (i,p,) iff b1 = f ) ) ) by A1; ::_thesis: verum
end;
correctness
coherence
Replace (i,p,) is FinSequence of D;
consistency
for b1 being FinSequence of D holds verum;
proof
reconsider i = i as Element of NAT by ORDINAL1:def_12;
 f +* (i,p) is FinSequence of D ;
hence  ( Replace (i,p,) is FinSequence of D & ( for b1 being FinSequence of D holds verum ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Replace FINSEQ_7:def_1_:_
 for D being non empty set
for f being FinSequence of D
for i being Nat
for p being Element of D holds
( ( 1 <= i & i <= len f implies Replace (f,i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) & ( ( not 1 <= i or not i <= len f ) implies Replace (f,i,p) = f ) );

theorem :: FINSEQ_7:5
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat holds len (Replace (f,i,p)) = len f by FUNCT_7:97;

theorem :: FINSEQ_7:6
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat holds rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:100;

theorem :: FINSEQ_7:7
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace (f,i,p))
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace (f,i,p))
let f be FinSequence of D; ::_thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace (f,i,p))
let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace (f,i,p))
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies p in rng (Replace (f,i,p)) )
assume  ( 1 <= i & i <= len f ) ; ::_thesis: p in rng (Replace (f,i,p))
then  i in dom f by FINSEQ_3:25;
hence  p in rng (Replace (f,i,p)) by FUNCT_7:102; ::_thesis: verum
end;

Lm2:  for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let f be FinSequence of D; ::_thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies (Replace (f,i,p)) . i = p )
assume  ( 1 <= i & i <= len f ) ; ::_thesis: (Replace (f,i,p)) . i = p
then  i in dom f by FINSEQ_3:25;
hence  (Replace (f,i,p)) . i = p by FUNCT_7:31; ::_thesis: verum
end;

theorem :: FINSEQ_7:8
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) /. i = p
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) /. i = p
let f be FinSequence of D; ::_thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) /. i = p
let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) /. i = p
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies (Replace (f,i,p)) /. i = p )
assume  ( 1 <= i & i <= len f ) ; ::_thesis: (Replace (f,i,p)) /. i = p
then  i in dom f by FINSEQ_3:25;
hence  (Replace (f,i,p)) /. i = p by FUNCT_7:36; ::_thesis: verum
end;

theorem :: FINSEQ_7:9
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
let f be FinSequence of D; ::_thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
let p be Element of D; ::_thesis: for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k )
assume that
A1: 1 <= i and
A2: i <= len f ; ::_thesis: for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
 i - 1 < i by XREAL_1:146;
then A3: i -' 1 < i by A1, XREAL_1:233;
A4: len ((f | (i -' 1)) ^ <*p*>) = (len (f | (i -' 1))) + (len <*p*>) by FINSEQ_1:22
.= (i -' 1) + (len <*p*>) by A2, A3, FINSEQ_1:59, XXREAL_0:2
.= (i -' 1) + 1 by FINSEQ_1:39
.= i by A1, XREAL_1:235 ;
let k be Nat; ::_thesis: ( 0 < k & k <= (len f) - i implies (Replace (f,i,p)) . (i + k) = (f /^ i) . k )
assume that
A5: 0 < k and
A6: k <= (len f) - i ; ::_thesis: (Replace (f,i,p)) . (i + k) = (f /^ i) . k
A7: 0 + 1 <= k by A5, INT_1:7;
len f = len (Replace (f,i,p)) by FUNCT_7:97
.= len (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) by A1, A2, Def1
.= i + (len (f /^ i)) by A4, FINSEQ_1:22 ;
then A8: k in dom (f /^ i) by A6, A7, FINSEQ_3:25;
 (Replace (f,i,p)) . (i + k) = (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) . ((len ((f | (i -' 1)) ^ <*p*>)) + k) by A1, A2, A4, Def1;
hence  (Replace (f,i,p)) . (i + k) = (f /^ i) . k by A8, FINSEQ_1:def_7; ::_thesis: verum
end;

theorem Th10: :: FINSEQ_7:10
for D being non empty set
for f being FinSequence of D
for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
let f be FinSequence of D; ::_thesis: for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
let p be Element of D; ::_thesis: for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
let k, i be Nat; ::_thesis: ( 1 <= k & k <= len f & k <> i implies (Replace (f,i,p)) /. k = f /. k )
assume A1: ( 1 <= k & k <= len f & k <> i ) ; ::_thesis: (Replace (f,i,p)) /. k = f /. k
reconsider i = i, k = k as Element of NAT by ORDINAL1:def_12;
 ( k <> i & k in dom f ) by A1, FINSEQ_3:25;
hence  (Replace (f,i,p)) /. k = f /. k by FUNCT_7:37; ::_thesis: verum
end;

theorem Th11: :: FINSEQ_7:11
for D being non empty set
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)
proof
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 that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; ::_thesis: 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) ; ::_thesis: verum
end;

theorem :: FINSEQ_7:12
for D being non empty set
for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*>
proof
let D be non empty set ; ::_thesis: for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*>
let p, q be Element of D; ::_thesis: Replace (<*p*>,1,q) = <*q*>
A1: 1 - 1 = 0 ;
set g = <*> D;
reconsider P = <*p*> ^ (<*> D) as FinSequence of D ;
A2: (<*p*> ^ (<*> D)) /^ 1 = <*> D by FINSEQ_6:45;
 1 <= len <*p*> by FINSEQ_1:39;
hence  Replace (<*p*>,1,q) = ((<*p*> | (1 -' 1)) ^ <*q*>) ^ (<*p*> /^ 1) by Def1
.= ((<*p*> | 0) ^ <*q*>) ^ (<*p*> /^ 1) by A1, XREAL_0:def_2
.= <*q*> ^ (<*p*> /^ 1) by FINSEQ_1:34
.= <*q*> ^ (P /^ 1) by FINSEQ_1:34
.= <*q*> by A2, FINSEQ_1:34 ;
::_thesis: verum
end;

theorem Th13: :: FINSEQ_7:13
for D being non empty set
for p1, p2, q being Element of D holds Replace (<*p1,p2*>,1,q) = <*q,p2*>
proof
let D be non empty set ; ::_thesis: for p1, p2, q being Element of D holds Replace (<*p1,p2*>,1,q) = <*q,p2*>
let p1, p2, q be Element of D; ::_thesis: Replace (<*p1,p2*>,1,q) = <*q,p2*>
set f = <*p1,p2*>;
A1: len <*p1,p2*> = 2 by FINSEQ_1:44;
then A2: 2 in dom <*p1,p2*> by FINSEQ_3:25;
 1 + 1 = len <*p1,p2*> by FINSEQ_1:44;
then A3: <*p1,p2*> /^ 1 = <*(<*p1,p2*> /. 2)*> by FINSEQ_5:30
.= <*(<*p1,p2*> . 2)*> by A2, PARTFUN1:def_6 ;
Replace (<*p1,p2*>,1,q) = ((<*p1,p2*> | (1 -' 1)) ^ <*q*>) ^ (<*p1,p2*> /^ 1) by A1, Def1
.= ((<*p1,p2*> | 0) ^ <*q*>) ^ (<*p1,p2*> /^ 1) by XREAL_1:232
.= ({} ^ <*q*>) ^ <*p2*> by A3, FINSEQ_1:44
.= <*q*> ^ <*p2*> by FINSEQ_1:34 ;
hence  Replace (<*p1,p2*>,1,q) = <*q,p2*> ; ::_thesis: verum
end;

theorem Th14: :: FINSEQ_7:14
for D being non empty set
for p1, p2, q being Element of D holds Replace (<*p1,p2*>,2,q) = <*p1,q*>
proof
let D be non empty set ; ::_thesis: for p1, p2, q being Element of D holds Replace (<*p1,p2*>,2,q) = <*p1,q*>
let p1, p2, q be Element of D; ::_thesis: Replace (<*p1,p2*>,2,q) = <*p1,q*>
set f = <*p1,p2*>;
A1: 2 -' 1 = (1 + 1) -' 1
.= 1 by NAT_D:34 ;
 len <*p1,p2*> = 2 by FINSEQ_1:44;
then A2: 1 in dom <*p1,p2*> by FINSEQ_3:25;
 2 <= len <*p1,p2*> by FINSEQ_1:44;
then  Replace (<*p1,p2*>,2,q) = ((<*p1,p2*> | (2 -' 1)) ^ <*q*>) ^ (<*p1,p2*> /^ 2) by Def1
.= ((<*p1,p2*> | 1) ^ <*q*>) ^ (<*p1,p2*> /^ (len <*p1,p2*>)) by A1, FINSEQ_1:44
.= ((<*p1,p2*> | 1) ^ <*q*>) ^ {} by RFINSEQ:27
.= (<*(<*p1,p2*> /. 1)*> ^ <*q*>) ^ {} by FINSEQ_5:20
.= <*(<*p1,p2*> /. 1)*> ^ <*q*> by FINSEQ_1:34
.= <*(<*p1,p2*> . 1)*> ^ <*q*> by A2, PARTFUN1:def_6
.= <*p1*> ^ <*q*> by FINSEQ_1:44 ;
hence  Replace (<*p1,p2*>,2,q) = <*p1,q*> ; ::_thesis: verum
end;

theorem Th15: :: FINSEQ_7:15
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
set f = <*p1,p2,p3*>;
 len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then  Replace (<*p1,p2,p3*>,1,q) = ((<*p1,p2,p3*> | (1 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by Def1
.= ((<*p1,p2,p3*> | 0) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by XREAL_1:232
.= <*q*> ^ (<*p1,p2,p3*> /^ 1) by FINSEQ_1:34
.= <*q*> ^ <*p2,p3*> by FINSEQ_6:47
.= (<*q*> ^ <*p2*>) ^ <*p3*> by FINSEQ_1:32 ;
hence  Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> ; ::_thesis: verum
end;

theorem Th16: :: FINSEQ_7:16
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
set f = <*p1,p2,p3*>;
A1: 2 -' 1 = (1 + 1) -' 1
.= 1 by NAT_D:34 ;
A2: len <*p1,p2,p3*> = 2 + 1 by FINSEQ_1:45;
A3: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then A4: 3 in dom <*p1,p2,p3*> by FINSEQ_3:25;
A5: 1 in dom <*p1,p2,p3*> by A3, FINSEQ_3:25;
Replace (<*p1,p2,p3*>,2,q) = ((<*p1,p2,p3*> | (2 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 2) by A3, Def1
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> /. 3)*> by A1, A2, FINSEQ_5:30
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> . 3)*> by A4, PARTFUN1:def_6
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*p3*> by FINSEQ_1:45
.= (<*(<*p1,p2,p3*> /. 1)*> ^ <*q*>) ^ <*p3*> by FINSEQ_5:20
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*q*>) ^ <*p3*> by A5, PARTFUN1:def_6
.= (<*p1*> ^ <*q*>) ^ <*p3*> by FINSEQ_1:45 ;
hence  Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> ; ::_thesis: verum
end;

theorem Th17: :: FINSEQ_7:17
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
let p1, p2, p3, q be Element of D; ::_thesis: Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
set f = <*p1,p2,p3*>;
A1: 3 -' 1 = (2 + 1) -' 1
.= 2 by NAT_D:34 ;
A2: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then A3: 1 in dom <*p1,p2,p3*> by FINSEQ_3:25;
A4: 2 in dom <*p1,p2,p3*> by A2, FINSEQ_3:25;
 3 <= len <*p1,p2,p3*> by FINSEQ_1:45;
then  Replace (<*p1,p2,p3*>,3,q) = ((<*p1,p2,p3*> | (3 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 3) by Def1
.= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ (<*p1,p2,p3*> /^ (len <*p1,p2,p3*>)) by A1, FINSEQ_1:45
.= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ {} by RFINSEQ:27
.= (<*p1,p2,p3*> | 2) ^ <*q*> by FINSEQ_1:34
.= <*(<*p1,p2,p3*> /. 1),(<*p1,p2,p3*> /. 2)*> ^ <*q*> by A2, FINSEQ_5:81
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> /. 2)*>) ^ <*q*> by A3, PARTFUN1:def_6
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by A4, PARTFUN1:def_6
.= (<*p1*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by FINSEQ_1:45
.= (<*p1*> ^ <*p2*>) ^ <*q*> by FINSEQ_1:45 ;
hence  Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*> ; ::_thesis: verum
end;

begin

registration
let f be FinSequence;
let i, j be Nat;
cluster Swap (f,i,j) ->  FinSequence-like ;
correctness
coherence
Swap (f,i,j) is FinSequence-like ;
proof
 dom (Swap (f,i,j)) = dom f by FUNCT_7:99;
hence  ex n being Nat st dom (Swap (f,i,j)) = Seg n by FINSEQ_1:def_2; :: according to FINSEQ_1:def_2 ::_thesis: verum
end;
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i, j be Nat;
:: original: Swap
redefine func Swap (f,i,j) ->  FinSequence of D equals :Def2: :: FINSEQ_7:def 2
 Replace ((Replace (f,i,(f /. j))),j,(f /. i)) if ( 1 <= i & i <= len f & 1 <= j & j <= len f )
otherwise f;
coherence
 Swap (f,i,j) is FinSequence of D
proof
 rng (Swap (f,i,j)) = rng f by FUNCT_7:103;
hence  rng (Swap (f,i,j)) c= D by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b1 = Swap (f,i,j) iff b1 = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( b1 = Swap (f,i,j) iff b1 = f ) ) )
proof
let IT be FinSequence of D; ::_thesis: ( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) ) )
thus  ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) ::_thesis: ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) )
proof
assume that
A1: ( 1 <= i & i <= len f ) and
A2: ( 1 <= j & j <= len f ) ; ::_thesis: ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) )
A3: j in dom f by A2, FINSEQ_3:25;
then A4: f /. j = f . j by PARTFUN1:def_6;
A5: i in dom f by A1, FINSEQ_3:25;
then  f /. i = f . i by PARTFUN1:def_6;
hence  ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) by A5, A3, A4, FUNCT_7:def_12; ::_thesis: verum
end;
assume  ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: ( IT = Swap (f,i,j) iff IT = f )
then  ( not i in dom f or not j in dom f ) by FINSEQ_3:25;
hence  ( IT = Swap (f,i,j) iff IT = f ) by FUNCT_7:def_12; ::_thesis: verum
end;
correctness
consistency
for b1 being FinSequence of D holds verum;
;
end;

:: deftheorem Def2 defines Swap FINSEQ_7:def_2_:_
 for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap (f,i,j) = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies Swap (f,i,j) = f ) );

theorem Th18: :: FINSEQ_7:18
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds len (Swap (f,i,j)) = len f
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat holds len (Swap (f,i,j)) = len f
let f be FinSequence of D; ::_thesis: for i, j being Nat holds len (Swap (f,i,j)) = len f
let i, j be Nat; ::_thesis: len (Swap (f,i,j)) = len f
 dom (Swap (f,i,j)) = dom f by FUNCT_7:99;
hence  len (Swap (f,i,j)) = len f by FINSEQ_3:29; ::_thesis: verum
end;

Lm3:  for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
let i, j be Nat; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) )
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
A5: i in dom f by A1, A2, FINSEQ_3:25;
set F = Replace (f,i,(f /. j));
A6: i <= len (Replace (f,i,(f /. j))) by A2, FUNCT_7:97;
A7: j <= len (Replace (f,i,(f /. j))) by A4, FUNCT_7:97;
A8: j in dom f by A3, A4, FINSEQ_3:25;
percases ( i = j or i <> j ) ;
supposeA9: i = j ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
(Swap (f,i,j)) . i = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i by A1, A2, A3, A4, Def2
.= f /. i by A1, A6, A9, Lm2
.= f . i by A5, PARTFUN1:def_6 ;
hence  ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A9; ::_thesis: verum
end;
supposeA10: i <> j ; ::_thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
A11: (Swap (f,i,j)) . j = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . j by A1, A2, A3, A4, Def2
.= f /. i by A3, A7, Lm2 ;
(Swap (f,i,j)) . i = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i by A1, A2, A3, A4, Def2
.= (Replace (f,i,(f /. j))) . i by A10, FUNCT_7:32
.= f /. j by A1, A2, Lm2 ;
hence  ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A5, A8, A11, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;

theorem Th19: :: FINSEQ_7:19
for D being non empty set
for f being FinSequence of D
for i being Nat holds Swap (f,i,i) = f
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i being Nat holds Swap (f,i,i) = f
let f be FinSequence of D; ::_thesis: for i being Nat holds Swap (f,i,i) = f
let i be Nat; ::_thesis: Swap (f,i,i) = f
reconsider i = i as Element of NAT by ORDINAL1:def_12;
percases ( ( 1 <= i & i <= len f ) or not 1 <= i or not i <= len f ) ;
suppose ( 1 <= i & i <= len f ) ; ::_thesis: Swap (f,i,i) = f
then  Swap (f,i,i) = Replace ((Replace (f,i,(f /. i))),i,(f /. i)) by Def2
.= Replace (f,i,(f /. i)) by FUNCT_7:38 ;
hence  Swap (f,i,i) = f by FUNCT_7:38; ::_thesis: verum
end;
suppose ( not 1 <= i or not i <= len f ) ; ::_thesis: Swap (f,i,i) = f
hence  Swap (f,i,i) = f by Def2; ::_thesis: verum
end;
end;
end;

theorem :: FINSEQ_7:20
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f
let f be FinSequence of D; ::_thesis: for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f
let i, j be Nat; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f
percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ;
supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f
A2: for k being Nat st 1 <= k & k <= len f holds
f . k = (Swap ((Swap (f,i,j)),j,i)) . k
proof
A3: i <= len (Swap (f,i,j)) by A1, Th18;
A4: j <= len (Swap (f,i,j)) by A1, Th18;
let k be Nat; ::_thesis: ( 1 <= k & k <= len f implies f . k = (Swap ((Swap (f,i,j)),j,i)) . k )
assume that
A5: 1 <= k and
A6: k <= len f ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k
A7: k <= len (Swap (f,i,j)) by A6, Th18;
now__::_thesis:_f_._k_=_(Swap_((Swap_(f,i,j)),j,i))_._k
percases ( i = k or i <> k ) ;
suppose i = k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k
then  (Swap ((Swap (f,i,j)),j,i)) . k = (Swap (f,k,j)) . j by A1, A7, A4, Lm3;
hence  f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A1, A5, A6, Lm3; ::_thesis: verum
end;
supposeA8: i <> k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k
now__::_thesis:_f_._k_=_(Swap_((Swap_(f,i,j)),j,i))_._k
percases ( j = k or j <> k ) ;
suppose j = k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k
then  (Swap ((Swap (f,i,j)),j,i)) . k = (Swap (f,i,k)) . i by A1, A7, A3, Lm3;
hence  f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A1, A5, A6, Lm3; ::_thesis: verum
end;
supposeA9: j <> k ; ::_thesis: f . k = (Swap ((Swap (f,i,j)),j,i)) . k
set S = Swap (f,i,j);
(Swap ((Swap (f,i,j)),j,i)) . k = (Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. i))),i,((Swap (f,i,j)) /. j))) . k by A1, A4, A3, Def2
.= (Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. i))) . k by A8, FUNCT_7:32
.= (Swap (f,i,j)) . k by A9, FUNCT_7:32
.= (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2
.= (Replace (f,i,(f /. j))) . k by A9, FUNCT_7:32 ;
hence  f . k = (Swap ((Swap (f,i,j)),j,i)) . k by A8, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence  f . k = (Swap ((Swap (f,i,j)),j,i)) . k ; ::_thesis: verum
end;
end;
end;
hence  f . k = (Swap ((Swap (f,i,j)),j,i)) . k ; ::_thesis: verum
end;
len (Swap ((Swap (f,i,j)),j,i)) = len (Swap (f,i,j)) by Th18
.= len f by Th18 ;
hence  Swap ((Swap (f,i,j)),j,i) = f by A2, FINSEQ_1:14; ::_thesis: verum
end;
supposeA10: ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: Swap ((Swap (f,i,j)),j,i) = f
then  Swap ((Swap (f,i,j)),j,i) = Swap (f,j,i) by Def2;
hence  Swap ((Swap (f,i,j)),j,i) = f by A10, Def2; ::_thesis: verum
end;
end;
end;

theorem Th21: :: FINSEQ_7:21
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)
let f be FinSequence of D; ::_thesis: for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)
let i, j be Nat; ::_thesis: Swap (f,i,j) = Swap (f,j,i)
percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ;
supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: Swap (f,i,j) = Swap (f,j,i)
set FJ = Replace (f,j,(f /. i));
set FI = Replace (f,i,(f /. j));
A2: for k being Nat st 1 <= k & k <= len (Swap (f,i,j)) holds
(Swap (f,i,j)) . k = (Swap (f,j,i)) . k
proof
A3: len (Swap (f,i,j)) = len f by Th18
.= len (Replace (f,j,(f /. i))) by FUNCT_7:97 ;
A4: len (Swap (f,i,j)) = len f by Th18
.= len (Replace (f,i,(f /. j))) by FUNCT_7:97 ;
let k be Nat; ::_thesis: ( 1 <= k & k <= len (Swap (f,i,j)) implies (Swap (f,i,j)) . k = (Swap (f,j,i)) . k )
assume that
A5: 1 <= k and
A6: k <= len (Swap (f,i,j)) ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
A7: k <= len f by A6, Th18;
now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k
percases ( i = k or i <> k ) ;
supposeA8: i = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k
percases ( j = k or j <> k ) ;
supposeA9: j = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
then (Swap (f,i,k)) . k = (Replace ((Replace (f,i,(f /. j))),k,(f /. i))) . k by A1, Def2
.= f /. i by A5, A6, A4, Lm2
.= (Replace ((Replace (f,j,(f /. i))),k,(f /. i))) . k by A5, A6, A3, Lm2
.= (Swap (f,k,i)) . k by A1, A8, A9, Def2 ;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A9; ::_thesis: verum
end;
supposeA10: j <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
(Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2
.= (Replace (f,k,(f /. j))) . k by A8, A10, FUNCT_7:32
.= f /. j by A5, A7, Lm2
.= (Replace ((Replace (f,j,(f /. i))),k,(f /. j))) . k by A5, A6, A3, Lm2 ;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, A8, Def2; ::_thesis: verum
end;
end;
end;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum
end;
supposeA11: i <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
now__::_thesis:_(Swap_(f,i,j))_._k_=_(Swap_(f,j,i))_._k
percases ( j = k or j <> k ) ;
supposeA12: j = k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
then (Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),k,(f /. i))) . k by A1, Def2
.= f /. i by A5, A6, A4, Lm2
.= (Replace (f,j,(f /. i))) . k by A5, A7, A12, Lm2
.= (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) . k by A11, FUNCT_7:32 ;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, Def2; ::_thesis: verum
end;
supposeA13: j <> k ; ::_thesis: (Swap (f,i,j)) . k = (Swap (f,j,i)) . k
(Swap (f,i,j)) . k = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k by A1, Def2
.= (Replace (f,i,(f /. j))) . k by A13, FUNCT_7:32
.= f . k by A11, FUNCT_7:32
.= (Replace (f,j,(f /. i))) . k by A13, FUNCT_7:32
.= (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) . k by A11, FUNCT_7:32 ;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k by A1, Def2; ::_thesis: verum
end;
end;
end;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum
end;
end;
end;
hence  (Swap (f,i,j)) . k = (Swap (f,j,i)) . k ; ::_thesis: verum
end;
len (Swap (f,i,j)) = len f by Th18
.= len (Swap (f,j,i)) by Th18 ;
hence  Swap (f,i,j) = Swap (f,j,i) by A2, FINSEQ_1:14; ::_thesis: verum
end;
supposeA14: ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: Swap (f,i,j) = Swap (f,j,i)
then  Swap (f,i,j) = f by Def2;
hence  Swap (f,i,j) = Swap (f,j,i) by A14, Def2; ::_thesis: verum
end;
end;
end;

theorem :: FINSEQ_7:22
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds rng (Swap (f,i,j)) = rng f by FUNCT_7:103;

theorem :: FINSEQ_7:23
for D being non empty set
for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*>
proof
let D be non empty set ; ::_thesis: for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*>
let p1, p2 be Element of D; ::_thesis: Swap (<*p1,p2*>,1,2) = <*p2,p1*>
set f = <*p1,p2*>;
A1: len <*p1,p2*> = 2 by FINSEQ_1:44;
then  1 in dom <*p1,p2*> by FINSEQ_3:25;
then A2: <*p1,p2*> /. 1 = <*p1,p2*> . 1 by PARTFUN1:def_6
.= p1 by FINSEQ_1:44 ;
 2 in dom <*p1,p2*> by A1, FINSEQ_3:25;
then A3: <*p1,p2*> /. 2 = <*p1,p2*> . 2 by PARTFUN1:def_6
.= p2 by FINSEQ_1:44 ;
Swap (<*p1,p2*>,1,2) = Replace ((Replace (<*p1,p2*>,1,(<*p1,p2*> /. 2))),2,(<*p1,p2*> /. 1)) by A1, Def2
.= Replace (<*p2,p2*>,2,(<*p1,p2*> /. 1)) by A3, Th13 ;
hence  Swap (<*p1,p2*>,1,2) = <*p2,p1*> by A2, Th14; ::_thesis: verum
end;

theorem :: FINSEQ_7:24
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>
let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>
set f = <*p1,p2,p3*>;
A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then  1 in dom <*p1,p2,p3*> by FINSEQ_3:25;
then A2: <*p1,p2,p3*> /. 1 = <*p1,p2,p3*> . 1 by PARTFUN1:def_6
.= p1 by FINSEQ_1:45 ;
 2 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25;
then A3: <*p1,p2,p3*> /. 2 = <*p1,p2,p3*> . 2 by PARTFUN1:def_6
.= p2 by FINSEQ_1:45 ;
Swap (<*p1,p2,p3*>,1,2) = Replace ((Replace (<*p1,p2,p3*>,1,(<*p1,p2,p3*> /. 2))),2,(<*p1,p2,p3*> /. 1)) by A1, Def2
.= Replace (<*p2,p2,p3*>,2,(<*p1,p2,p3*> /. 1)) by A3, Th15 ;
hence  Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*> by A2, Th16; ::_thesis: verum
end;

theorem :: FINSEQ_7:25
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>
let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>
set f = <*p1,p2,p3*>;
A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then  1 in dom <*p1,p2,p3*> by FINSEQ_3:25;
then A2: <*p1,p2,p3*> /. 1 = <*p1,p2,p3*> . 1 by PARTFUN1:def_6
.= p1 by FINSEQ_1:45 ;
 3 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25;
then A3: <*p1,p2,p3*> /. 3 = <*p1,p2,p3*> . 3 by PARTFUN1:def_6
.= p3 by FINSEQ_1:45 ;
Swap (<*p1,p2,p3*>,1,3) = Replace ((Replace (<*p1,p2,p3*>,1,(<*p1,p2,p3*> /. 3))),3,(<*p1,p2,p3*> /. 1)) by A1, Def2
.= Replace (<*p3,p2,p3*>,3,(<*p1,p2,p3*> /. 1)) by A3, Th15 ;
hence  Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*> by A2, Th17; ::_thesis: verum
end;

theorem :: FINSEQ_7:26
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>
proof
let D be non empty set ; ::_thesis: for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>
let p1, p2, p3 be Element of D; ::_thesis: Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>
set f = <*p1,p2,p3*>;
A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then  2 in dom <*p1,p2,p3*> by FINSEQ_3:25;
then A2: <*p1,p2,p3*> /. 2 = <*p1,p2,p3*> . 2 by PARTFUN1:def_6
.= p2 by FINSEQ_1:45 ;
 3 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25;
then A3: <*p1,p2,p3*> /. 3 = <*p1,p2,p3*> . 3 by PARTFUN1:def_6
.= p3 by FINSEQ_1:45 ;
Swap (<*p1,p2,p3*>,2,3) = Replace ((Replace (<*p1,p2,p3*>,2,(<*p1,p2,p3*> /. 3))),3,(<*p1,p2,p3*> /. 2)) by A1, Def2
.= Replace (<*p1,p3,p3*>,3,(<*p1,p2,p3*> /. 2)) by A3, Th16 ;
hence  Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*> by A2, Th17; ::_thesis: verum
end;

theorem Th27: :: FINSEQ_7:27
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
let i, j be Nat; ::_thesis: ( 1 <= i & i < j & j <= len f implies Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; ::_thesis: Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
A4: ( i <= len f & 1 <= j ) by A1, A2, A3, XXREAL_0:2;
Swap (f,i,j) = Swap (f,j,i) by Th21
.= Replace ((Replace (f,j,(f /. i))),i,(f /. j)) by A1, A3, A4, Def2 ;
hence  Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) by A1, A2, A3, Th11; ::_thesis: verum
end;

theorem :: FINSEQ_7:28
for D being non empty set
for f being FinSequence of D
for i being Nat st 1 < i & i <= len f holds
Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i being Nat st 1 < i & i <= len f holds
Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
let f be FinSequence of D; ::_thesis: for i being Nat st 1 < i & i <= len f holds
Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
let i be Nat; ::_thesis: ( 1 < i & i <= len f implies Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) )
assume  ( 1 < i & i <= len f ) ; ::_thesis: Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
then  Swap (f,1,i) = ((((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by Th27
.= ((((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by XREAL_1:232
.= ((<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) by FINSEQ_1:34 ;
hence  Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) by NAT_D:45; ::_thesis: verum
end;

theorem :: FINSEQ_7:29
for D being non empty set
for f being FinSequence of D
for i being Nat st 1 <= i & i < len f holds
Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i being Nat st 1 <= i & i < len f holds
Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
let f be FinSequence of D; ::_thesis: for i being Nat st 1 <= i & i < len f holds
Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
let i be Nat; ::_thesis: ( 1 <= i & i < len f implies Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> )
assume  ( 1 <= i & i < len f ) ; ::_thesis: Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
then  Swap (f,i,(len f)) = ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ (len f)) by Th27
.= ((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} by RFINSEQ:27 ;
hence  Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> by FINSEQ_1:34; ::_thesis: verum
end;

Lm4:  for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k
let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k
let i, k, j be Nat; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k )
percases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ;
supposeA1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k )
assume that
A2: i <> k and
A3: j <> k ; ::_thesis: (Swap (f,i,j)) . k = f . k
(Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . k = (Replace (f,i,(f /. j))) . k by A3, FUNCT_7:32
.= f . k by A2, FUNCT_7:32 ;
hence  (Swap (f,i,j)) . k = f . k by A1, Def2; ::_thesis: verum
end;
suppose ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; ::_thesis: ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k )
hence  ( i <> k & j <> k implies (Swap (f,i,j)) . k = f . k ) by Def2; ::_thesis: verum
end;
end;
end;

theorem Th30: :: FINSEQ_7:30
for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k
let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k
let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= k & k <= len f implies (Swap (f,i,j)) /. k = f /. k )
assume that
A1: ( i <> k & j <> k ) and
A2: 1 <= k and
A3: k <= len f ; ::_thesis: (Swap (f,i,j)) /. k = f /. k
A4: k in dom f by A2, A3, FINSEQ_3:25;
 k <= len (Swap (f,i,j)) by A3, Th18;
then  k in dom (Swap (f,i,j)) by A2, FINSEQ_3:25;
hence (Swap (f,i,j)) /. k = (Swap (f,i,j)) . k by PARTFUN1:def_6
.= f . k by A1, Lm4
.= f /. k by A4, PARTFUN1:def_6 ;
::_thesis: verum
end;

theorem Th31: :: FINSEQ_7:31
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )
let f be FinSequence of D; ::_thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )
let i, j be Nat; ::_thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) )
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; ::_thesis: ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )
A5: i in dom f by A1, A2, FINSEQ_3:25;
set F = Swap (f,i,j);
 j <= len (Swap (f,i,j)) by A4, Th18;
then  j in dom (Swap (f,i,j)) by A3, FINSEQ_3:25;
then A6: (Swap (f,i,j)) /. j = (Swap (f,i,j)) . j by PARTFUN1:def_6
.= f . i by A1, A2, A3, A4, Lm3
.= f /. i by A5, PARTFUN1:def_6 ;
A7: j in dom f by A3, A4, FINSEQ_3:25;
 i <= len (Swap (f,i,j)) by A2, Th18;
then  i in dom (Swap (f,i,j)) by A1, FINSEQ_3:25;
then (Swap (f,i,j)) /. i = (Swap (f,i,j)) . i by PARTFUN1:def_6
.= f . j by A1, A2, A3, A4, Lm3
.= f /. j by A7, PARTFUN1:def_6 ;
hence  ( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i ) by A6; ::_thesis: verum
end;

begin

theorem Th32: :: FINSEQ_7:32
for D being 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)
proof
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 that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; ::_thesis: 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;
percases ( i = j or i < j or i > j ) by XXREAL_0:1;
supposeA6: i = j ; ::_thesis: 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; ::_thesis: verum
end;
supposeA7: i < j ; ::_thesis: 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; ::_thesis: verum
end;
supposeA24: i > j ; ::_thesis: 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; ::_thesis: verum
end;
end;
end;

theorem Th33: :: FINSEQ_7:33
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for p being Element of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let f be FinSequence of D; ::_thesis: for p being Element of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let p be Element of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) )
assume that
A1: i <> k and
A2: j <> k and
A3: 1 <= i and
A4: i <= len f and
A5: 1 <= j and
A6: j <= len f ; ::_thesis: Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
 ( i <= len (Replace (f,k,p)) & j <= len (Replace (f,k,p)) ) by A4, A6, FUNCT_7:97;
hence  Swap ((Replace (f,k,p)),i,j) = Replace ((Replace ((Replace (f,k,p)),i,((Replace (f,k,p)) /. j))),j,((Replace (f,k,p)) /. i)) by A3, A5, Def2
.= Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,((Replace (f,k,p)) /. i)) by A2, A5, A6, Th10
.= Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,(f /. i)) by A1, A3, A4, Th10
.= Replace ((Replace ((Replace (f,i,(f /. j))),k,p)),j,(f /. i)) by A1, FUNCT_7:33
.= Replace ((Replace ((Replace (f,i,(f /. j))),j,(f /. i))),k,p) by A2, FUNCT_7:33
.= Replace ((Swap (f,i,j)),k,p) by A3, A4, A5, A6, Def2 ;
::_thesis: verum
end;

theorem :: FINSEQ_7:34
for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j)
let f be FinSequence of D; ::_thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j)
let i, k, j be Nat; ::_thesis: ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f implies Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j) )
assume that
A1: ( i <> k & j <> k ) and
A2: 1 <= i and
A3: i <= len f and
A4: 1 <= j and
A5: j <= len f and
A6: 1 <= k and
A7: k <= len f ; ::_thesis: Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j)
A8: ( i <= len (Replace (f,i,(f /. k))) & j <= len (Replace (f,i,(f /. k))) ) by A3, A5, FUNCT_7:97;
 ( j <= len (Swap (f,i,j)) & k <= len (Swap (f,i,j)) ) by A5, A7, Th18;
hence  Swap ((Swap (f,i,j)),j,k) = Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. k))),k,((Swap (f,i,j)) /. j)) by A4, A6, Def2
.= Replace ((Replace ((Swap (f,i,j)),j,((Swap (f,i,j)) /. k))),k,(f /. i)) by A2, A3, A4, A5, Th31
.= Replace ((Replace ((Swap (f,i,j)),j,(f /. k))),k,(f /. i)) by A1, A6, A7, Th30
.= Replace ((Replace ((Swap (f,j,i)),j,(f /. k))),k,(f /. i)) by Th21
.= Replace ((Swap ((Replace (f,i,(f /. k))),j,i)),k,(f /. i)) by A2, A3, A4, A5, Th32
.= Swap ((Replace ((Replace (f,i,(f /. k))),k,(f /. i))),j,i) by A1, A2, A4, A8, Th33
.= Swap ((Swap (f,i,k)),j,i) by A2, A3, A6, A7, Def2
.= Swap ((Swap (f,i,k)),i,j) by Th21 ;
::_thesis: verum
end;

theorem :: FINSEQ_7:35
for D being non empty set
for f being FinSequence of D
for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds
Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds
Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j)
let f be FinSequence of D; ::_thesis: for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds
Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j)
let i, k, j, l be Nat; ::_thesis: ( i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f implies Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) )
assume that
A1: ( i <> k & j <> k ) and
A2: ( l <> i & l <> j ) and
A3: 1 <= i and
A4: i <= len f and
A5: 1 <= j and
A6: j <= len f and
A7: 1 <= k and
A8: k <= len f and
A9: 1 <= l and
A10: l <= len f ; ::_thesis: Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j)
A11: ( i <= len (Replace (f,k,(f /. l))) & j <= len (Replace (f,k,(f /. l))) ) by A4, A6, FUNCT_7:97;
set F = Swap (f,i,j);
 ( k <= len (Swap (f,i,j)) & l <= len (Swap (f,i,j)) ) by A8, A10, Th18;
then  Swap ((Swap (f,i,j)),k,l) = Replace ((Replace ((Swap (f,i,j)),k,((Swap (f,i,j)) /. l))),l,((Swap (f,i,j)) /. k)) by A7, A9, Def2
.= Replace ((Replace ((Swap (f,i,j)),k,((Swap (f,i,j)) /. l))),l,(f /. k)) by A1, A7, A8, Th30
.= Replace ((Replace ((Swap (f,i,j)),k,(f /. l))),l,(f /. k)) by A2, A9, A10, Th30
.= Replace ((Replace ((Swap (f,j,i)),k,(f /. l))),l,(f /. k)) by Th21
.= Replace ((Swap ((Replace (f,k,(f /. l))),j,i)),l,(f /. k)) by A1, A3, A4, A5, A6, Th33
.= Swap ((Replace ((Replace (f,k,(f /. l))),l,(f /. k))),j,i) by A2, A3, A5, A11, Th33
.= Swap ((Swap (f,k,l)),j,i) by A7, A8, A9, A10, Def2
.= Swap ((Swap (f,k,l)),i,j) by Th21 ;
hence  Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j) ; ::_thesis: verum
end;