A1: ( sin is_differentiable_on ].0 ,1.[ & cos is_differentiable_on ].0 ,1.[ ) by Th72, Th73, FDIFF_1:34;
A2: for th being Real st th in ].0 ,1.[ holds
cos . th <> 0

proof

let th be Real; :: thesis: ( th in ].0 ,1.[ implies cos . th <> 0 )
assume A3: th in ].0 ,1.[ ; :: thesis: cos . th <> 0
A4: ].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
thus cos . th <> 0 by A3, A4, Th74; :: thesis: verum

end;

A5: for th being real number st th in ].0 ,1.[ holds
diff tan ,th > 0

proof

let th be real number ; :: thesis: ( th in ].0 ,1.[ implies diff tan ,th > 0 )
assume A6: th in ].0 ,1.[ ; :: thesis: diff tan ,th > 0
A7: ( th is Real & cos is_differentiable_in th ) by Th68, XREAL_0:def 1;
A8: sin is_differentiable_in th by Th69;
A9: cos . th <> 0 by A2, A6;
A10: diff tan ,th = (((diff sin ,th) * (cos . th)) - ((diff cos ,th) * (sin . th))) / ((cos . th) ^2 ) by A7, A8, A9, FDIFF_2:14
.= (((cos . th) * (cos . th)) - ((diff cos ,th) * (sin . th))) / ((cos . th) ^2 ) by Th69
.= (((cos . th) * (cos . th)) - ((- (sin . th)) * (sin . th))) / ((cos . th) ^2 ) by Th68
.= (((cos . th) ^2 ) + ((sin . th) * (sin . th))) / ((cos . th) ^2 )
.= 1 / ((cos . th) ^2 ) by Th31 ;
A11: (cos . th) ^2 > 0 by A9, SQUARE_1:74;
thus diff tan ,th > 0 by A10, A11; :: thesis: verum

end;

thus ( tan is_differentiable_on ].0 ,1.[ & ( for th being real number st th in ].0 ,1.[ holds
diff tan ,th > 0 ) ) by A1, A2, A5, FDIFF_2:21; :: thesis: verum