for i being Nat ex l being quasi-loci st len l = i