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:27;
set F = Swap f,i,j;
j <= len (Swap f,i,j) by A4, Th20;
then j in dom (Swap f,i,j) by A3, FINSEQ_3:27;
then A6: (Swap f,i,j) /. j = (Swap f,i,j) . j by PARTFUN1:def 8
.= f . i by A1, A2, A3, A4, Lm3
.= f /. i by A5, PARTFUN1:def 8 ;
A7: j in dom f by A3, A4, FINSEQ_3:27;
i <= len (Swap f,i,j) by A2, Th20;
then i in dom (Swap f,i,j) by A1, FINSEQ_3:27;
then (Swap f,i,j) /. i = (Swap f,i,j) . i by PARTFUN1:def 8
.= f . j by A1, A2, A3, A4, Lm3
.= f /. j by A7, PARTFUN1:def 8 ;
hence ( (Swap f,i,j) /. i = f /. j & (Swap f,i,j) /. j = f /. i ) by A6; :: thesis: verum