let D be non empty set ; :: thesis: for f being FinSequence of D
for i being Nat holds Swap (f,i,i) = f
let f be FinSequence of D; :: thesis: for i being Nat holds Swap (f,i,i) = f
let i be Nat; :: thesis: Swap (f,i,i) = f
reconsider i = i as Element of NAT by ORDINAL1:def 12;

per cases ( ( 1 <= i & i <= len f ) or not 1 <= i or not i <= len f ) ;

suppose ( 1 <= i & i <= len f ) ; :: thesis: Swap (f,i,i) = f

then Swap (f,i,i) = Replace ((Replace (f,i,(f /. i))),i,(f /. i)) by Def2
.= Replace (f,i,(f /. i)) by FUNCT_7:38 ;
hence Swap (f,i,i) = f by FUNCT_7:38; :: thesis: verum

end;

suppose ( not 1 <= i or not i <= len f ) ; :: thesis: Swap (f,i,i) = f

hence Swap (f,i,i) = f by Def2; :: thesis: verum

end;

end;