Equalization is one of the applications of adaptive filtering. Its role consists of eliminating the inter-symbol interference caused by the noise in the transmission environment. To get an output matching as much as possible to the desired response, uncountable adaptive algorithms are used to regulate the filter or the equalizer coefficients. To decrease the filtering complexity, the equalizer can be implemented in the frequency domain where time convolution is replaced by frequency multiplication; this method offers low complexity growth in comparison with the time domain approach. This technique requires the use of the Fast Fourier Transform (FFT) modules. One possible implementation for the equalizer is based on the Fast LMS algorithm. Verifying the correctness of the equalizer is very challenging because of many reasons. First the equalizer implementation is based on an iterative algorithm, second, it contains multiple FFT and IFFT blocks, and finally, it contains multiple mathematical operators using several number domains. In this work we will use HOL theorem proving technique in order to provide error analysis for an implementation of the Frequency domain equalizer based on Fast LMS algorithm. This analysis is required to show that the error generated in the implementation of the Fast LMS algorithm conforms to the required accuracy of conversion in the Equalizer design to operate properly. The formal analysis of the algorithm intends to show that, when converting from one number domain to another, the algorithm produces the same values with an accepted error margin caused by the round-off error accumulation.