environ
vocabularies HIDDEN, INTEGRA1, INTEGRA2, FINSEQ_1, SEQ_1, SEQ_2, ORDINAL2, ARYTM_1, RELAT_1, FUNCT_1, PARTFUN1, XBOOLE_0, FUNCT_3, INTEGR15, REALSET1, XCMPLX_0, COMPLEX1, COMSEQ_1, SETWISEO, SUBSET_1, NUMBERS, CARD_1, ORDINAL4, NAT_1, TARSKI, CARD_3, MEASURE7, ARYTM_3, BINOP_2, XXREAL_0, XXREAL_2, INTEGRA5, VALUED_1, REAL_1, XXREAL_1, FUNCT_2, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, REAL_1, RCOMP_1, VALUED_1, RELSET_1, PARTFUN1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, BINOP_2, BINOP_1, SETWOP_2, RVSUM_1, XXREAL_0, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, INTEGR15, MESFUN6C, COMSEQ_1, COMSEQ_2, COMSEQ_3;
definitions ;
theorems XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_0, INTEGRA1, COMSEQ_3, RFUNCT_1, COMPLEX1, RELSET_1, BINOP_2, FINSOP_1, NAT_1, XXREAL_0, RELAT_1, ORDINAL1, XREAL_1, FINSEQ_1, RVSUM_1, FUNCT_1, FUNCT_2, INTEGRA5, FINSEQ_3, INTEGRA6, INTEGR15, VALUED_1, MESFUN6C, COMSEQ_2;
schemes FUNCT_2, FINSEQ_1, NAT_1;
registrations NUMBERS, XREAL_0, INTEGRA1, FUNCT_2, BINOP_2, MEMBERED, ORDINAL1, VALUED_0, RELSET_1, FINSEQ_1, MEASURE5, XCMPLX_0;
constructors HIDDEN, REAL_1, MONOID_0, MEASURE6, BINOP_2, INTEGRA5, RELSET_1, INTEGR15, FINSOP_1, SETWISEO, COMSEQ_2, COMSEQ_3, MESFUN6C, SQUARE_1, SEQ_2, INTEGRA3, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, INTEGRA5, INTEGR15, FINSEQ_1, COMPLEX1, RVSUM_1;
expansions XBOOLE_0, INTEGRA5, COMPLEX1;
Lm2:
Sum (<*> COMPLEX) = 0
by BINOP_2:1, FINSOP_1:10;
Lm3:
for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x
Lm4:
for f being PartFunc of REAL,COMPLEX
for A being Subset of REAL holds
( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A )