dom (tan | [.0,1.]) = (dom tan) /\ [.0,1.] by RELAT_1:61;
then dom (tan | [.0,1.]) = [.0,1.] by Th69, XBOOLE_1:28;
hence ( dom (tan | [.0,1.]) = [.0,1.] & ( for th being Real st th in [.0,1.] holds
(tan | [.0,1.]) . th = tan . th ) ) by FUNCT_1:47; :: thesis: verum