A2: dom (@ ((@ sin) |^ 0)) = REAL by FUNCT_2:def 1;
(@ sin) |^ 0 = REAL --> 1 by Lm6;
then A4: for x being Real st x in ['0,(PI / 2)'] holds
(@ ((@ sin) |^ 0)) . x = 1 by FUNCOP_1:7;
['0,(PI / 2)'] = [.0,(PI / 2).] by COMPTRIG:5, INTEGRA5:def 3;
then ( 0 in ['0,(PI / 2)'] & PI / 2 in ['0,(PI / 2)'] ) by COMPTRIG:5, XXREAL_1:1;
then integral ((@ ((@ sin) |^ 0)),0,(PI / 2)) = 1 * ((PI / 2) - 0) by COMPTRIG:5, A2, A4, INTEGRA6:27
.= PI / 2 ;
hence integral ((@ ((@ sin) |^ 0)),0,(PI / 2)) = PI / 2 ; :: thesis: verum