A1: sin is_differentiable_on ].(- (PI / 2)),(PI / 2).[

proof

].(- (PI / 2)),(PI / 2).[ is open by RCOMP_1:25;
hence sin is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_1:34, SIN_COS:73; :: thesis: verum

end;

for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff sin ,x > 0

proof

let x be Real; :: thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies diff sin ,x > 0 )
assume x in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: diff sin ,x > 0
then 0 < cos . x by Th27;
hence diff sin ,x > 0 by SIN_COS:73; :: thesis: verum

end;

hence sin | ].(- (PI / 2)),(PI / 2).[ is increasing by A1, Lm0, ROLLE:9, SIN_COS:27; :: thesis: verum