A1: [.0 ,1.] \ (cos " {0 }) c= (dom cos ) \ (cos " {0 }) by Th27, XBOOLE_1:33;
[.0 ,1.] /\ (cos " {0 }) = {}

proof

assume [.0 ,1.] /\ (cos " {0 }) <> {} ; :: thesis: contradiction
then consider rr being set such that
A4: rr in [.0 ,1.] /\ (cos " {0 }) by XBOOLE_0:def 1;
A5: rr in [.0 ,1.] by A4, XBOOLE_0:def 4;
A6: rr in cos " {0 } by A4, XBOOLE_0:def 4;
A7: cos . rr <> 0 by A5, Th74;
cos . rr in {0 } by A6, FUNCT_1:def 13;
hence contradiction by A7, 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 Th27, XBOOLE_1:19;
then A12: [.0 ,1.] c= dom tan by RFUNCT_1:def 4;
].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
hence ( [.0 ,1.] c= dom tan & ].0 ,1.[ c= dom tan ) by A12, XBOOLE_1:1; :: thesis: verum