theorem :: COMPTRIG:30

rng (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- 1),1.]