A1: [.0,1.] \ (cos " {0}) c= (dom cos) \ (cos " {0}) by Th24, XBOOLE_1:33;
[.0,1.] /\ (cos " {0}) = {}
proof
assume [.0,1.] /\ (cos " {0}) <> {} ; :: thesis: contradiction
then consider rr being object such that
A2: rr in [.0,1.] /\ (cos " {0}) by XBOOLE_0:def 1;
A3: rr in [.0,1.] by A2, XBOOLE_0:def 4;
A4: rr in cos " {0} by A2, XBOOLE_0:def 4;
A5: cos . rr <> 0 by A3, Th68;
cos . rr in {0} by A4, FUNCT_1:def 7;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum
end;
then [.0,1.] misses cos " {0} by XBOOLE_0:def 7;
then [.0,1.] c= (dom cos) \ (cos " {0}) by A1, XBOOLE_1:83;
then [.0,1.] c= (dom sin) /\ ((dom cos) \ (cos " {0})) by Th24, XBOOLE_1:19;
then A6: [.0,1.] c= dom tan by RFUNCT_1:def 1;
].0,1.[ c= [.0,1.] by XXREAL_1:25;
hence ( [.0,1.] c= dom tan & ].0,1.[ c= dom tan ) by A6, XBOOLE_1:1; :: thesis: verum