let IT be FinSequence of D; :: thesis: ( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) ) )
thus ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) :: thesis: ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( IT = Swap (f,i,j) iff IT = f ) )

proof

assume that
A1: ( 1 <= i & i <= len f ) and
A2: ( 1 <= j & j <= len f ) ; :: thesis: ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) )
A3: j in dom f by A2, FINSEQ_3:25;
then A4: f /. j = f . j by PARTFUN1:def 6;
A5: i in dom f by A1, FINSEQ_3:25;
then f /. i = f . i by PARTFUN1:def 6;
hence ( IT = Swap (f,i,j) iff IT = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) by A5, A3, A4, FUNCT_7:def 12; :: thesis: verum

end;

assume ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; :: thesis: ( IT = Swap (f,i,j) iff IT = f )
then ( not i in dom f or not j in dom f ) by FINSEQ_3:25;
hence ( IT = Swap (f,i,j) iff IT = f ) by FUNCT_7:def 12; :: thesis: verum