Metamathematical interpretation of the fan theorem

Brouwer's fan theorem states that if (a) a function $f$ assigns a natural number to every element of a given fan then (b) its values depend on $N$ initial members of an argument only, where $N$ is sufficiently large. Elements are treated there as choise sequences. If one treats them as recursive functions then the statement “(a) implies (b)” is known to be false. However we prove that if (a) is provable in a certain formal system of constructive analysis which is correct with respect to the interpretation of sequences as recursive functions then (b) holds under the same interpretation.
The system is obtained from Kleene–Vesley system of intuitionistic analysis by deleting bar theorem and Brouwer principle and adding Markov's scheme.