A1: ( sin is_differentiable_on ].0,1.[ & cos is_differentiable_on ].0,1.[ ) by Th66, Th67, FDIFF_1:26;
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
].0,1.[ c= [.0,1.] by XXREAL_1:25;
hence cos . th <> 0 by A3, Th68; :: thesis: verum

end;

for th being Real st th in ].0,1.[ holds
diff (tan,th) > 0

proof

let th be Real; :: thesis: ( th in ].0,1.[ implies diff (tan,th) > 0 )
assume A4: th in ].0,1.[ ; :: thesis: diff (tan,th) > 0
A5: ( th is Real & cos is_differentiable_in th ) by Th62;
A6: sin is_differentiable_in th by Th63;
A7: cos . th <> 0 by A2, A4;
then A8: diff (tan,th) = (((diff (sin,th)) * (cos . th)) - ((diff (cos,th)) * (sin . th))) / ((cos . th) ^2) by A5, A6, FDIFF_2:14
.= (((cos . th) * (cos . th)) - ((diff (cos,th)) * (sin . th))) / ((cos . th) ^2) by Th63
.= (((cos . th) * (cos . th)) - ((- (sin . th)) * (sin . th))) / ((cos . th) ^2) by Th62
.= (((cos . th) ^2) + ((sin . th) * (sin . th))) / ((cos . th) ^2)
.= 1 / ((cos . th) ^2) by Th28 ;
(cos . th) ^2 > 0 by A7, SQUARE_1:12;
hence diff (tan,th) > 0 by A8; :: thesis: verum

end;

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