environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FUNCT_2, FINSET_1, FUNCT_1, CARD_1, FUNCOP_1, COMPLEX1, ALGSTR_0, RLVECT_2, TARSKI, NAT_1, CLVECT_1, FINSEQ_1, VALUED_1, RELAT_1, PARTFUN1, XXREAL_0, RLVECT_1, CARD_3, SUPINF_2, RLSUB_1, ARYTM_3, ARYTM_1, QC_LANG1, BINOP_1, ZFMISC_1, RUSUB_4, REAL_1, REALSET1, XCMPLX_0, CONVEX1, SETFAM_1, CSSPACE, PROB_2, CONVEX4, PRE_POLY, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, DOMAIN_1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PRE_POLY, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_4, ALGSTR_0, RLVECT_1, SETFAM_1, STRUCT_0, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, FINSET_1, PARTFUN1, FUNCOP_1, CARD_1, VALUED_1, XCMPLX_0, COMPLEX1, RVSUM_1, RUSUB_4, RUSUB_5, BINOP_1, REAL_1, RLVECT_2, CLVECT_1, CSSPACE, REALSET1;
definitions FUNCT_1, TARSKI, XBOOLE_0, ALGSTR_0;
theorems RVSUM_1, SETFAM_1, ENUMSET1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, NAT_1, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, COMPLEX1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, FINSOP_1, CLVECT_1, CSSPACE, CONVEX1, PARTFUN1, XREAL_0, VALUED_1, ALGSTR_0, PRE_POLY, XCMPLX_0;
schemes DOMAIN_1, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
registrations STRUCT_0, MEMBERED, XXREAL_0, CSSPACE, RLVECT_1, RELSET_1, FINSET_1, XREAL_0, SUBSET_1, XCMPLX_0, CLVECT_1, NUMBERS, NAT_1, FUNCT_2, VALUED_1, VALUED_0, CARD_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, BINOP_1, FUNCOP_1, REAL_1, FINSEQ_4, COMPLEX1, REALSET1, BINOP_2, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, CSSPACE, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, BINOP_1, RELAT_1, STRUCT_0, REALSET1, FINSEQ_1, CLVECT_1, COMPLEX1, RVSUM_1, XCMPLX_0, ALGSTR_0, RUSUB_4, RUSUB_5;
expansions TARSKI, BINOP_1, STRUCT_0, CLVECT_1, ALGSTR_0;
Lm2:
for V being ComplexLinearSpace
for M being Subset of V
for z1, z2 being Complex st ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds
(z1 * M) + (z2 * M) c= (z1 + z2) * M
Lm3:
for V being ComplexLinearSpace
for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)