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 ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; :: thesis: ( IT = Swap f,i,j iff IT = Replace (Replace f,i,(f /. j)),j,(f /. i) )
then A1: ( i in dom f & j in dom f ) by FINSEQ_3:27;
then ( f /. i = f . i & f /. j = f . j ) by PARTFUN1:def 8;
hence ( IT = Swap f,i,j iff IT = Replace (Replace f,i,(f /. j)),j,(f /. i) ) by A1, 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:27;
hence ( IT = Swap f,i,j iff IT = f ) by FUNCT_7:def 12; :: thesis: verum