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