A1: dom (tan | [.0 ,1.]) = (dom tan ) /\ [.0 ,1.] by RELAT_1:90;
A2: dom (tan | [.0 ,1.]) = [.0 ,1.] by A1, Th75, XBOOLE_1:28;
thus ( dom (tan | [.0 ,1.]) = [.0 ,1.] & ( for th being real number st th in [.0 ,1.] holds
(tan | [.0 ,1.]) . th = tan . th ) ) by A2, FUNCT_1:70; :: thesis: verum