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

A9: 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.[
A13: th1 < th by A12, XXREAL_1:4;
A14: th < th2 by A12, XXREAL_1:4;
A15: th < 1 by A7, A14, XXREAL_0:2;
thus th in ].0 ,1.[ by A4, A13, A15, 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.]
A18: th1 <= th by A17, XXREAL_1:1;
A19: th <= th2 by A17, XXREAL_1:1;
A20: th <= 1 by A7, A19, XXREAL_0:2;
thus th in [.0 ,1.] by A4, A18, A20, XXREAL_1:1; :: thesis: verum

end;

A21: ].th1,th2.[ c= ].0 ,1.[ by A11, SUBSET_1:7;
A22: tan is_differentiable_on ].th1,th2.[ by A21, Lm16, FDIFF_1:34;
A23: ( [.th1,th2.] c= [.0 ,1.] & tan | [.th1,th2.] is continuous ) by A16, Th76, FCONT_1:17, SUBSET_1:7;
consider r being Real such that
A24: ( r in ].th1,th2.[ & diff tan ,r = 0 ) by A1, A2, A3, A10, A22, A23, 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.[
A28: th2 < th by A27, XXREAL_1:4;
A29: th < th1 by A27, XXREAL_1:4;
A30: th < 1 by A5, A29, XXREAL_0:2;
thus th in ].0 ,1.[ by A6, A28, A30, 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.]
A33: th2 <= th by A32, XXREAL_1:1;
A34: th <= th1 by A32, XXREAL_1:1;
A35: th <= 1 by A5, A34, XXREAL_0:2;
thus th in [.0 ,1.] by A6, A33, A35, XXREAL_1:1; :: thesis: verum

end;

A36: ].th2,th1.[ c= ].0 ,1.[ by A26, SUBSET_1:7;
A37: tan is_differentiable_on ].th2,th1.[ by A36, Lm16, FDIFF_1:34;
A38: ( [.th2,th1.] c= [.0 ,1.] & tan | [.th2,th1.] is continuous ) by A31, Th76, FCONT_1:17, SUBSET_1:7;
consider r being Real such that
A39: ( r in ].th2,th1.[ & diff tan ,r = 0 ) by A1, A2, A3, A25, A37, A38, 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;

thus contradiction by A9, Lm16; :: thesis: verum