A1: 0 in ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:4;
then tan . 0 = 0 / (cos . 0) by Th1, RFUNCT_1:def 1, SIN_COS:30
.= 0 ;
hence ( tan . 0 = 0 & tan 0 = 0 ) by A1, Th13; :: thesis: verum