theorem Th1: :: FDIFF_8:1

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