set Z = ].0 ,(PI / 2).[;
[.0 ,(PI / 2).[ = ].0 ,(PI / 2).[ \/ {0 } by XXREAL_1:131;
then ].0 ,(PI / 2).[ c= [.0 ,(PI / 2).[ by XBOOLE_1:7;
then A1: ].0 ,(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1;
then A2: sec is_differentiable_on ].0 ,(PI / 2).[ by FDIFF_9:4;
for x being Real st x in ].0 ,(PI / 2).[ holds
diff sec ,x = (sin . x) / ((cos . x) ^2 )

proof

let x be Real; :: thesis: ( x in ].0 ,(PI / 2).[ implies diff sec ,x = (sin . x) / ((cos . x) ^2 ) )
assume A3: x in ].0 ,(PI / 2).[ ; :: thesis: diff sec ,x = (sin . x) / ((cos . x) ^2 )
diff sec ,x = (sec `| ].0 ,(PI / 2).[) . 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 ].0 ,(PI / 2).[ & ( for x being Real st x in ].0 ,(PI / 2).[ holds
diff sec ,x = (sin . x) / ((cos . x) ^2 ) ) ) by A1, FDIFF_9:4; :: thesis: verum