environ
vocabularies HIDDEN, NUMBERS, NAT_1, FINSEQ_1, VALUED_0, FINSEQ_2, CARD_1, RELAT_1, SUBSET_1, XBOOLE_0, FUNCT_1, TARSKI, XREAL_0, ORDINAL4, BINOP_1, BINOP_2, ARYTM_1, ARYTM_3, SQUARE_1, FUNCOP_1, REAL_1, FINSEQOP, ZFMISC_1, VALUED_1, XXREAL_0, CARD_3, XCMPLX_0, SETWISEO, SETWOP_2, FINSOP_1, RVSUM_1, FUNCT_7, ORDINAL1;
notations HIDDEN, TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0, XBOOLE_0, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, BINOP_2, SETWISEO, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, VALUED_1, NAT_1, FINSOP_1, FINSEQOP, SETWOP_2;
definitions BINOP_1, FINSEQOP, FINSEQ_1;
theorems SQUARE_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, SETWOP_2, RELAT_1, FINSOP_1, XREAL_0, ZFMISC_1, XCMPLX_0, BINOP_2, SETWISEO, XREAL_1, NUMBERS, XBOOLE_1, FINSEQ_3, ORDINAL1, VALUED_0, VALUED_1, CARD_1, RFUNCT_1, INT_1, TARSKI;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, NAT_1, BINOP_2, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, FINSEQ_4, CARD_1, INT_1;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, BINOP_2, VALUED_1, FINSEQOP, FINSEQ_4, FINSOP_1, SETWOP_2, RELSET_1, XXREAL_1, REAL_1, FINSEQ_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, SQUARE_1, FINSEQ_2, VALUED_1, FINSEQ_4;
expansions BINOP_1, FINSEQOP, FINSEQ_1;
Lm1:
for r, r1 being Real holds (multreal [;] (r,(id REAL))) . r1 = r * r1
Lm2:
for F being real-valued FinSequence holds F is FinSequence of REAL
Lm3:
for F being empty FinSequence holds Product F = 1
Lm4:
for p being complex-valued FinSequence st len p <> 0 holds
ex q being complex-valued FinSequence ex d being Complex st p = q ^ <*d*>
Lm5:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
theorem
for
r1,
r2,
r3,
r4 being
Real holds
Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4