theorem Th16: :: BASEL_1:16

dom tan = union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum }