set Z = ].(PI / 2),PI .[;
PI / 2 < PI / 1 by XREAL_1:78;
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, XBOOLE_1:1;
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 )
diff sec ,x = (sec `| ].(PI / 2),PI .[) . x by A2, A3, FDIFF_1:def 8
.= (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