environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_1, RELAT_1, ARYTM_1, ARYTM_3, XXREAL_0, REAL_1, FINSEQ_1, FUNCT_1, CARD_3, ORDINAL4, TARSKI, PARTFUN1, XBOOLE_0, HAHNBAN1, XCMPLX_0, COMPLFLD, SUPINF_2, COMPLEX1, GROUP_1, POWER, STRUCT_0, NAT_1, RLVECT_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES, POLYNOM1, ALGSEQ_1, POLYNOM3, POLYNOM2, VECTSP_2, MESFUNC1, AFINSQ_1, FUNCT_4, CQC_LANG, CFCONT_1, FUNCOP_1, VALUED_1, FUNCT_2, SEQ_4, XXREAL_2, COMSEQ_1, VALUED_0, SEQ_2, ORDINAL2, SEQ_1, COMPTRIG, RFINSEQ, POLYNOM5, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, POWER, BINOP_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_4, POLYNOM1, RVSUM_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCSDOM, VECTSP_2, VECTSP_1, RFINSEQ, CFCONT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, XXREAL_0, COMSEQ_1, COMSEQ_2, NAT_D, COMPLFLD, HAHNBAN1, ALGSEQ_1, POLYNOM3, POLYNOM4, FUNCT_7, RECDEF_1, GROUP_1;
definitions TARSKI, ALGSEQ_1, XBOOLE_0, ALGSTR_0, XXREAL_2, COMSEQ_2;
theorems XREAL_0, TARSKI, ENUMSET1, NAT_1, POWER, INT_1, ABSVALUE, FUNCT_1, FUNCT_2, FUNCT_7, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, FUNCOP_1, TBSP_1, RFINSEQ, PRE_FF, CFCONT_1, TOPREAL3, INTEGRA5, RLVECT_1, VECTSP_1, RVSUM_1, SEQ_2, SEQM_3, SEQ_4, COMSEQ_2, COMSEQ_3, CFUNCT_1, FVSUM_1, GROUP_1, ALGSEQ_1, COMPLEX1, COMPLFLD, HAHNBAN1, POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM4, XBOOLE_0, XCMPLX_1, VECTSP_2, XREAL_1, XXREAL_0, FINSOP_1, NORMSP_1, PARTFUN1, ORDINAL1, VALUED_1, CARD_1, NAT_D, VALUED_0, XCMPLX_0, SEQ_1;
schemes NAT_1, FUNCT_2, FINSEQ_2, FINSEQ_1, FINSEQ_4, SEQ_1, CFCONT_1, DOMAIN_1, FUNCT_7;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, GROUP_1, VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM3, POLYNOM4, VALUED_0, VALUED_1, CARD_1, SEQ_2, CFUNCT_1, SEQ_1;
constructors HIDDEN, FINSEQ_4, ENUMSET1, REAL_1, SEQ_4, FINSOP_1, COMSEQ_2, RVSUM_1, CFCONT_1, RFINSEQ, NAT_D, FUNCSDOM, VECTSP_2, ALGSTR_1, MATRIX_1, HAHNBAN1, POLYNOM1, POLYNOM4, RECDEF_1, BINOP_2, POWER, SEQ_2, RELSET_1, FUNCT_7, FVSUM_1, ALGSEQ_1, ORDINAL1, SEQ_1, GROUP_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XBOOLE_0, RVSUM_1, POLYNOM3, HAHNBAN1, STRUCT_0, ALGSTR_0, XCMPLX_0;
expansions TARSKI, ALGSEQ_1, COMSEQ_2;
theorem Th3:
for
x,
y being
Real st ( for
c being
Real st
c > 0 &
c < 1 holds
c * x >= y ) holds
y <= 0
Lm1:
for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
by Th3;
Lm2:
for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L