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