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;