let i, j be Nat; :: thesis: for D being non empty set
for f being FinSequence of D 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 D be non empty set ; :: thesis: for f being FinSequence of D 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: ( 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: len (Replace (f,i,(f /. j))) = len f by FINSEQ_7:5;
A6: len (Swap (f,i,j)) = len f by FINSEQ_7:18;
then (Swap (f,i,j)) /. j = (Swap (f,i,j)) . j by A3, A4, FINSEQ_4:15;
then A7: (Swap (f,i,j)) . j = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) /. j by A1, A2, A3, A4, FINSEQ_7:def 2
.= f /. i by A3, A4, A5, FINSEQ_7:8
.= f . i by A1, A2, FINSEQ_4:15 ;
A8: Swap (f,i,j) = Swap (f,j,i) by FINSEQ_7:21;
A9: len (Replace (f,j,(f /. i))) = len f by FINSEQ_7:5;
(Swap (f,i,j)) /. i = (Swap (f,i,j)) . i by A1, A2, A6, FINSEQ_4:15;
then (Swap (f,i,j)) . i = (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) /. i by A1, A2, A3, A4, A8, FINSEQ_7:def 2
.= f /. j by A1, A2, A9, FINSEQ_7:8
.= f . j by A3, A4, FINSEQ_4:15 ;
hence ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A7; :: thesis: verum