for x being Real st x in dom tan holds
cos . x <> 0