let IT be FinSequence of D; ( ( 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)) ) )
( ( 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 )
;
( 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;
verum
end;
assume
( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f )
; ( 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; verum