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;
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)
then diff (sec,x) = (sec `| ].0,(PI / 2).[) . 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 ].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