environ
vocabularies HIDDEN, REAL_1, SUBSET_1, NUMBERS, RCOMP_1, PARTFUN1, PREPOWER, SQUARE_1, NEWTON, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, POWER, ARYTM_1, SIN_COS, FUNCT_1, TARSKI, XXREAL_1, VALUED_1, SIN_COS6, FDIFF_1, TAYLOR_1, XBOOLE_0, ORDINAL4, LIMFUNC1;
notations HIDDEN, TARSKI, SUBSET_1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2, RCOMP_1, ORDINAL1, XCMPLX_0, XREAL_0, NEWTON, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, VALUED_1, FDIFF_1, PREPOWER, POWER, SIN_COS6, LIMFUNC1;
definitions ;
theorems FUNCT_1, SIN_COS6, FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_4, POWER, SQUARE_1, FDIFF_1, TARSKI, PREPOWER, RFUNCT_1, XREAL_1, SIN_COS, SIN_COS5, NEWTON, VALUED_1, XXREAL_1, XREAL_0;
schemes ;
registrations RELSET_1, NUMBERS, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, SIN_COS, SQUARE_1, PREPOWER;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, SIN_COS6, TAYLOR_1, VALUED_1, RELSET_1, NEWTON;
requirements HIDDEN, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities SQUARE_1, RCOMP_1, LIMFUNC1, VALUED_1;
expansions ;
Lm1:
for x being Real holds 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x)
Lm2:
for x being Real holds 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x)
Lm3:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;