environ
vocabularies HIDDEN, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2, CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, MEMBERED, ORDERS_1, RELAT_1, RLVECT_1, RLVECT_2, RUSUB_4, SEMI_AF1, SETFAM_1, TARSKI, TOPS_1, RLAFFIN1, RLAFFIN2, ZFMISC_1, REAL_1, CARD_3, XXREAL_0, NAT_1, SUBSET_1, NUMBERS, ORDINAL1, STRUCT_0, SUPINF_2, ORDINAL4, VALUED_1, XREAL_0, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, ORDERS_1, CARD_1, XREAL_0, REAL_1, FINSET_1, SETFAM_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, RELSET_1, FINSEQ_1, STRUCT_0, FINSEQ_2, FINSEQOP, RVSUM_1, RLVECT_1, RLVECT_2, RUSUB_4, CONVEX1, CONVEX2, CONVEX3, RLAFFIN1, FUNCT_4, FUNCOP_1, MEMBERED, XXREAL_2;
definitions TARSKI, XBOOLE_0;
theorems SUBSET_1, CARD_1, CARD_2, CONVEX1, CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, NAT_1, MEMBERED, PARTFUN1, RELAT_1, RLAFFIN1, RLTOPSP1, RUSUB_4, RLVECT_2, RLVECT_3, RLVECT_4, RVSUM_1, STIRL2_1, SIMPLEX0, TARSKI, WELLORD2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, RLVECT_1;
schemes FRAENKEL, FUNCT_2, NAT_1;
registrations CARD_1, FINSET_1, FINSEQ_2, FUNCT_2, MEMBERED, NAT_1, NUMBERS, RELAT_1, RLVECT_1, STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, RLAFFIN1, FUNCOP_1, SETFAM_1, XXREAL_2, ABIAN, RELSET_1, RLVECT_2, ORDINAL1;
constructors HIDDEN, BINOP_2, CONVEX1, CONVEX3, DOMAIN_1, FINSEQOP, REAL_1, RVSUM_1, RUSUB_5, SETFAM_1, RLAFFIN1, SIMPLEX0, XXREAL_2, FUNCT_4, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ORDERS_1, RLVECT_2, XBOOLE_0, ORDINAL1;
expansions RLVECT_2, TARSKI, XBOOLE_0;
Lm1:
for r being Real
for V being RealLinearSpace
for v, u, w being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
Lm2:
for V being non empty RLSStruct
for A being Subset of V holds Int A c= conv A
by Def1;
reconsider jj = 1 as Real ;
Lm3:
for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )