let D be non empty set ; for f being FinSequence of D
for i, j being Nat holds len (Swap (f,i,j)) = len f
let f be FinSequence of D; for i, j being Nat holds len (Swap (f,i,j)) = len f
let i, j be Nat; len (Swap (f,i,j)) = len f
dom (Swap (f,i,j)) = dom f
by FUNCT_7:99;
hence
len (Swap (f,i,j)) = len f
by FINSEQ_3:29; verum