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; :: thesis: ( x in ].(PI / 2),PI.[ implies diff (sec,x) = (sin . x) / ((cos . x) ^2) )
assume A3: x in ].(PI / 2),PI.[ ; :: thesis: 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) ; :: thesis: 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; :: thesis: verum