environ
vocabularies HIDDEN, ALGSTR_0, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2, CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, MONOID_0, ORDERS_1, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RUSUB_4, SEMI_AF1, SETFAM_1, SUBSET_1, TARSKI, CLASSES1, SUPINF_2, RLVECT_5, REAL_1, NUMBERS, NAT_1, CARD_3, XXREAL_0, STRUCT_0, ZFMISC_1, RLAFFIN1, ORDINAL1, ORDINAL4, PARTFUN1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDERS_1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FINSET_1, SETFAM_1, DOMAIN_1, ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, STRUCT_0, FINSEQ_2, FINSEQ_3, FINSEQOP, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RLSUB_1, RLSUB_2, RUSUB_4, CONVEX1, CONVEX2, CONVEX3;
definitions CONVEX1, RLVECT_3, RUSUB_4, TARSKI, XBOOLE_0;
theorems CARD_2, CONVEX1, CONVEX3, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQOP, FINSET_1, FINSOP_1, FUNCT_1, FUNCT_2, MATRPROB, NAT_1, ORDERS_1, ORDINAL1, PARTFUN1, RELAT_1, RFINSEQ, RLTOPSP1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_4, RLVECT_5, RLSUB_1, RLSUB_2, RUSUB_4, RVSUM_1, SETFAM_1, STIRL2_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ZFMISC_1, CARD_1;
schemes FRAENKEL, FUNCT_1, FUNCT_2, NAT_1, TREES_2, XFAMILY;
registrations BINOP_2, CARD_1, CONVEX1, FINSET_1, FINSEQ_2, FUNCT_1, FUNCT_2, NAT_1, NUMBERS, RELAT_1, RLVECT_1, RLVECT_3, RUSUB_4, STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, RLVECT_5, RELSET_1, RLVECT_2, ORDINAL1;
constructors HIDDEN, BINOP_1, BINOP_2, CLASSES1, CONVEX1, CONVEX3, FINSEQOP, FINSOP_1, MATRLIN, ORDERS_1, REALSET1, REAL_1, RLVECT_3, RLVECT_5, RVSUM_1, RLSUB_2, RUSUB_5, SETWISEO, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities CONVEX1, FINSEQ_1, RLVECT_2, RUSUB_4, RVSUM_1, STRUCT_0, SUBSET_1, XBOOLE_0;
expansions CONVEX1, FINSEQ_1, RLVECT_2, RLVECT_3, RUSUB_4, STRUCT_0, TARSKI, XBOOLE_0;
Lm1:
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
Lm3:
for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
Lm4:
for V being non empty addLoopStr
for A being Subset of V
for v being Element of V holds card (v + A) c= card A
Lm5:
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
Lm6:
for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
Lm7:
for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
Lm8:
for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
Lm9:
for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
reconsider jj = 1 as Real ;