environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_0, CARD_1, ARYTM_3, NAT_1, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, COMPLFLD, COMPLEX1, PARTFUN1, CARD_3, STRUCT_0, REAL_1, ORDINAL4, FINSET_1, UPROOTS, ARYTM_1, POLYNOM2, AFINSQ_1, GROUP_1, INT_1, HAHNBAN1, SQUARE_1, POWER, SIN_COS, BINOP_1, ALGSTR_0, FINSEQ_2, MOD_2, VECTSP_1, VECTSP_2, REALSET1, ZFMISC_1, SUPINF_2, COMPTRIG, RAT_1, PREPOWER, NEWTON, XCMPLX_0, INT_2, BINOP_2, GROUP_2, POLYNOM1, POLYNOM3, FUNCT_4, ALGSEQ_1, VALUED_0, POLYNOM5, SGRAPH1, PRE_POLY, GRAPH_2, MESFUNC1, UNIROOTS;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, REALSET1, CARD_1, ORDINAL1, NUMBERS, XREAL_0, ZFMISC_1, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, SQUARE_1, INT_1, INT_2, NAT_D, PREPOWER, POWER, BINOP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, RAT_1, DOMAIN_1, FINSET_1, BINOP_2, RVSUM_1, STRUCT_0, ALGSTR_0, VECTSP_2, VECTSP_1, GROUP_4, ALGSEQ_1, COMPLFLD, HAHNBAN1, POLYNOM3, POLYNOM4, POLYNOM5, COMPTRIG, GROUP_2, NEWTON, GROUP_1, MOD_2, GRAPH_2, PRE_POLY, FVSUM_1, UPROOTS, SIN_COS, FUNCT_7, FINSEQ_2;
definitions TARSKI, GROUP_1, XBOOLE_0;
theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, PREPOWER, COMPTRIG, COMPLFLD, BINOP_1, XCMPLX_1, COMPLEX1, HAHNBAN1, SIN_COS, POWER, SIN_COS2, POLYNOM5, INT_1, COMPLEX2, XCMPLX_0, XREAL_0, SQUARE_1, RVSUM_1, FVSUM_1, FINSEQ_3, FINSEQ_2, FINSEQ_4, POLYNOM4, INT_2, WSIERP_1, NAT_2, PEPIN, POLYNOM3, COMPUT_1, NORMSP_1, FUNCT_7, ALGSEQ_1, RLVECT_1, NEWTON, POLYNOM2, MATRIX_3, VECTSP_2, MOD_2, CARD_2, GRAPH_2, FINSEQ_5, UPROOTS, GROUP_2, BINOP_2, XREAL_1, XXREAL_0, GROUP_4, FUNCOP_1, ORDINAL1, FINSOP_1, NAT_D, PARTFUN1, PRE_POLY;
schemes NAT_1, FUNCT_2, FINSEQ_1, INT_1, RECDEF_1;
registrations RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, FINSEQ_2, REALSET1, WSIERP_1, STRUCT_0, GROUP_1, VECTSP_1, COMPLFLD, QUOFIELD, POLYNOM3, POLYNOM5, VALUED_0, ALGSTR_0, POWER, RELSET_1, PRE_POLY, PREPOWER, SQUARE_1, NEWTON, SIN_COS, ORDINAL1;
constructors HIDDEN, WELLORD2, BINOP_1, REAL_1, SQUARE_1, NAT_D, FINSEQOP, FINSOP_1, RVSUM_1, PREPOWER, POWER, REALSET1, SIN_COS, GROUP_4, MOD_2, MATRIX_1, HAHNBAN1, GRAPH_2, POLYNOM4, POLYNOM5, UPROOTS, RECDEF_1, BINOP_2, RELSET_1, PBOOLE, FUNCT_7, NEWTON, FVSUM_1, ALGSEQ_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities GROUP_1, XBOOLE_0, BINOP_1, REALSET1, SQUARE_1, HAHNBAN1, POLYNOM3, FINSEQ_2, COMPLEX1, GROUP_4, ALGSTR_0, STRUCT_0, POLYNOM5;
expansions TARSKI, GROUP_1, XBOOLE_0;
Lm1:
for k being Element of NAT holds
( not k is zero iff 1 <= k )
Lm2:
for f being FinSequence
for n, i being Element of NAT st i <= n holds
(f | (Seg n)) | (Seg i) = f | (Seg i)
by FINSEQ_1:5, RELAT_1:74;
Lm3:
Z_3 is finite
by MOD_2:def 20;
Lm4:
unital_poly (F_Complex,1) = <%(- (1_ F_Complex)),(1_ F_Complex)%>
;