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 13;

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:40 ;
hence Swap f,i,i = f by FUNCT_7:40; :: 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;