let i be integer number ; :: thesis: sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is one-to-one
set Q = [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).];
sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is increasing by Th53;
then (sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).]) | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is increasing ;
then (sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).]) | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is one-to-one by FCONT_3:16;
hence sin | [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).] is one-to-one by RELAT_1:101; :: thesis: verum