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

proof

assume A3: [.0 ,1.] /\ (cos " {0 }) <> {} ; :: thesis: contradiction
consider rr being set such that
A4: rr in [.0 ,1.] /\ (cos " {0 }) by A3, 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;
A8: cos . rr in {0 } by A6, FUNCT_1:def 13;
thus contradiction by A7, A8, TARSKI:def 1; :: thesis: verum

end;

A9: [.0 ,1.] misses cos " {0 } by A2, XBOOLE_0:def 7;
A10: [.0 ,1.] c= (dom cos ) \ (cos " {0 }) by A1, A9, XBOOLE_1:83;
A11: [.0 ,1.] c= (dom sin ) /\ ((dom cos ) \ (cos " {0 })) by A10, Th27, XBOOLE_1:19;
A12: [.0 ,1.] c= dom tan by A11, RFUNCT_1:def 4;
A13: ].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
thus ( [.0 ,1.] c= dom tan & ].0 ,1.[ c= dom tan ) by A12, A13, XBOOLE_1:1; :: thesis: verum