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 A1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; :: thesis: ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
A2: len (Swap f,i,j) = len f by FINSEQ_7:20;
then A3: (Swap f,i,j) /. j = (Swap f,i,j) . j by A1, FINSEQ_4:24;
A4: (Swap f,i,j) /. i = (Swap f,i,j) . i by A1, A2, FINSEQ_4:24;
A5: len (Replace f,j,(f /. i)) = len f by FINSEQ_7:7;
A6: len (Replace f,i,(f /. j)) = len f by FINSEQ_7:7;
A7: (Swap f,i,j) . j = (Replace (Replace f,i,(f /. j)),j,(f /. i)) /. j by A1, A3, FINSEQ_7:def 2
.= f /. i by A6, A1, FINSEQ_7:10
.= f . i by A1, FINSEQ_4:24 ;
Swap f,i,j = Swap f,j,i by FINSEQ_7:23;
then (Swap f,i,j) . i = (Replace (Replace f,j,(f /. i)),i,(f /. j)) /. i by A1, A4, FINSEQ_7:def 2
.= f /. j by A5, A1, FINSEQ_7:10
.= f . j by A1, FINSEQ_4:24 ;
hence ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i ) by A7; :: thesis: verum