let D be non empty set ; 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; for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)
let i, j be Nat; Swap (f,i,j) = Swap (f,j,i)
per cases
( ( 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 )
;
suppose A1:
( 1
<= i &
i <= len f & 1
<= j &
j <= len f )
;
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;
( 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))
;
(Swap (f,i,j)) . k = (Swap (f,j,i)) . k
A7:
k <= len f
by A6, Th18;
now (Swap (f,i,j)) . k = (Swap (f,j,i)) . kper cases
( i = k or i <> k )
;
suppose A8:
i = k
;
(Swap (f,i,j)) . k = (Swap (f,j,i)) . know (Swap (f,i,j)) . k = (Swap (f,j,i)) . kper cases
( j = k or j <> k )
;
suppose A9:
j = k
;
(Swap (f,i,j)) . k = (Swap (f,j,i)) . kthen (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;
verum end; suppose A10:
j <> k
;
(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;
verum end; end; end; hence
(Swap (f,i,j)) . k = (Swap (f,j,i)) . k
;
verum end; suppose A11:
i <> k
;
(Swap (f,i,j)) . k = (Swap (f,j,i)) . know (Swap (f,i,j)) . k = (Swap (f,j,i)) . kper cases
( j = k or j <> k )
;
suppose A12:
j = k
;
(Swap (f,i,j)) . k = (Swap (f,j,i)) . kthen (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;
verum end; suppose A13:
j <> k
;
(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;
verum end; end; end; hence
(Swap (f,i,j)) . k = (Swap (f,j,i)) . k
;
verum end; end; end;
hence
(Swap (f,i,j)) . k = (Swap (f,j,i)) . k
;
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;
verum end; end;