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