set Z = ].(PI / 2),PI.[;
PI / 2 < PI / 1
by XREAL_1:76;
then
].(PI / 2),PI.] = ].(PI / 2),PI.[ \/ {PI}
by XXREAL_1:132;
then
].(PI / 2),PI.[ c= ].(PI / 2),PI.]
by XBOOLE_1:7;
then A1:
].(PI / 2),PI.[ c= dom sec
by Th2;
then A2:
sec is_differentiable_on ].(PI / 2),PI.[
by FDIFF_9:4;
for x being Real st x in ].(PI / 2),PI.[ holds
diff (sec,x) = (sin . x) / ((cos . x) ^2)
proof
let x be
Real;
( x in ].(PI / 2),PI.[ implies diff (sec,x) = (sin . x) / ((cos . x) ^2) )
assume A3:
x in ].(PI / 2),PI.[
;
diff (sec,x) = (sin . x) / ((cos . x) ^2)
then diff (
sec,
x) =
(sec `| ].(PI / 2),PI.[) . x
by A2, FDIFF_1:def 7
.=
(sin . x) / ((cos . x) ^2)
by A1, A3, FDIFF_9:4
;
hence
diff (
sec,
x)
= (sin . x) / ((cos . x) ^2)
;
verum
end;
hence
( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds
diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
by A1, FDIFF_9:4; verum