let D be non empty set ; :: thesis: 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; :: thesis: for i, j being Nat holds len (Swap (f,i,j)) = len f
let i, j be Nat; :: thesis: 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; :: thesis: verum