let th1, th2 be real number ; :: thesis: ( th1 in ].0 ,1.[ & th2 in ].0 ,1.[ & tan . th1 = tan . th2 implies th1 = th2 )
assume that
A1: th1 in ].0 ,1.[ and
A2: th2 in ].0 ,1.[ and
A3: tan . th1 = tan . th2 ; :: thesis: th1 = th2
A4: 0 < th1 by A1, XXREAL_1:4;
A5: th1 < 1 by A1, XXREAL_1:4;
A6: 0 < th2 by A2, XXREAL_1:4;
A7: th2 < 1 by A2, XXREAL_1:4;
assume A8: th1 <> th2 ; :: thesis: contradiction

now

per cases ( th1 < th2 or th2 < th1 ) by A8, XXREAL_0:1;

suppose A10: th1 < th2 ; :: thesis: ex th being Real st
( th in ].0 ,1.[ & diff tan ,th = 0 )

A11: for th being Real st th in ].th1,th2.[ holds
th in ].0 ,1.[

proof

let th be Real; :: thesis: ( th in ].th1,th2.[ implies th in ].0 ,1.[ )
assume A12: th in ].th1,th2.[ ; :: thesis: th in ].0 ,1.[
then A13: th1 < th by XXREAL_1:4;
th < th2 by A12, XXREAL_1:4;
then th < 1 by A7, XXREAL_0:2;
hence th in ].0 ,1.[ by A4, A13, XXREAL_1:4; :: thesis: verum

end;

A16: for th being Real st th in [.th1,th2.] holds
th in [.0 ,1.]

proof

let th be Real; :: thesis: ( th in [.th1,th2.] implies th in [.0 ,1.] )
assume A17: th in [.th1,th2.] ; :: thesis: th in [.0 ,1.]
then A18: th1 <= th by XXREAL_1:1;
th <= th2 by A17, XXREAL_1:1;
then th <= 1 by A7, XXREAL_0:2;
hence th in [.0 ,1.] by A4, A18, XXREAL_1:1; :: thesis: verum

end;

].th1,th2.[ c= ].0 ,1.[ by A11, SUBSET_1:7;
then A22: tan is_differentiable_on ].th1,th2.[ by Lm16, FDIFF_1:34;
( [.th1,th2.] c= [.0 ,1.] & tan | [.th1,th2.] is continuous ) by A16, Th76, FCONT_1:17, SUBSET_1:7;
then consider r being Real such that
A24: ( r in ].th1,th2.[ & diff tan ,r = 0 ) by A1, A2, A3, A10, A22, Th75, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0 ,1.[ & diff tan ,th = 0 )
thus ( th in ].0 ,1.[ & diff tan ,th = 0 ) by A11, A24; :: thesis: verum

end;

suppose A25: th2 < th1 ; :: thesis: ex th being Real st
( th in ].0 ,1.[ & diff tan ,th = 0 )

A26: for th being Real st th in ].th2,th1.[ holds
th in ].0 ,1.[

proof

let th be Real; :: thesis: ( th in ].th2,th1.[ implies th in ].0 ,1.[ )
assume A27: th in ].th2,th1.[ ; :: thesis: th in ].0 ,1.[
then A28: th2 < th by XXREAL_1:4;
th < th1 by A27, XXREAL_1:4;
then th < 1 by A5, XXREAL_0:2;
hence th in ].0 ,1.[ by A6, A28, XXREAL_1:4; :: thesis: verum

end;

A31: for th being Real st th in [.th2,th1.] holds
th in [.0 ,1.]

proof

let th be Real; :: thesis: ( th in [.th2,th1.] implies th in [.0 ,1.] )
assume A32: th in [.th2,th1.] ; :: thesis: th in [.0 ,1.]
then A33: th2 <= th by XXREAL_1:1;
th <= th1 by A32, XXREAL_1:1;
then th <= 1 by A5, XXREAL_0:2;
hence th in [.0 ,1.] by A6, A33, XXREAL_1:1; :: thesis: verum

end;

].th2,th1.[ c= ].0 ,1.[ by A26, SUBSET_1:7;
then A37: tan is_differentiable_on ].th2,th1.[ by Lm16, FDIFF_1:34;
( [.th2,th1.] c= [.0 ,1.] & tan | [.th2,th1.] is continuous ) by A31, Th76, FCONT_1:17, SUBSET_1:7;
then consider r being Real such that
A39: ( r in ].th2,th1.[ & diff tan ,r = 0 ) by A1, A2, A3, A25, A37, Th75, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0 ,1.[ & diff tan ,th = 0 )
thus ( th in ].0 ,1.[ & diff tan ,th = 0 ) by A26, A39; :: thesis: verum

end;

end;

end;

hence contradiction by Lm16; :: thesis: verum