environ
vocabularies HIDDEN, FINSEQ_1, FINSEQ_2, ARYTM_1, FUNCT_1, RELAT_1, BINOP_1, SETWISEO, SQUARE_1, FUNCOP_1, RVSUM_1, RVSUM_2, CARD_3, XBOOLE_0, COMPLEX1, XCMPLX_0, VALUED_0, BINOP_2, ZFMISC_1, NUMBERS, SUBSET_1, NAT_1, TARSKI, ORDINAL4, ARYTM_3, CARD_1, VALUED_1, REAL_1;
notations HIDDEN, TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0, XBOOLE_0, XCMPLX_0, XREAL_0, COMPLEX1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, BINOP_2, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_4, FINSEQOP, SETWOP_2, RVSUM_1;
definitions BINOP_1, FINSEQ_1;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, SETWOP_2, RELAT_1, FINSOP_1, ZFMISC_1, XCMPLX_0, BINOP_2, FINSEQ_3, VALUED_0, VALUED_1, RFUNCT_1, RVSUM_1, SEQ_4, CARD_1;
schemes NAT_1, FUNCT_2;
registrations FUNCT_1, FUNCT_2, FUNCOP_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, RVSUM_1, CARD_1, XCMPLX_0, NAT_1;
constructors HIDDEN, BINOP_1, COMPLEX1, SETWISEO, SQUARE_1, BINOP_2, FINSEQOP, FINSOP_1, RELSET_1, RVSUM_1, SEQ_4, CARD_1, CARD_3;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, SQUARE_1, VALUED_1, XCMPLX_0, RVSUM_1, XBOOLE_0, SEQ_4;
expansions ;
Lm1:
for c, c1 being Complex holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
Lm2:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
Lm3:
for F being empty FinSequence holds Product F = 1