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:101;
hence len (Swap f,i,j) = len f by FINSEQ_3:31; :: thesis: verum