environ
vocabularies HIDDEN, REAL_1, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, VALUED_1, ORDINAL4, ARYTM_3, RELAT_1, PARTFUN1, NAT_1, INT_1, CARD_3, CARD_1, SUPINF_2, TARSKI, FUNCT_2, ARYTM_1, RLVECT_3, RLVECT_X, XXREAL_0, VALUED_0, FUNCT_4, FUNCOP_1, FINSEQ_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, VALUED_0, FINSEQ_1, FINSEQ_2, STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, RUSUB_4, VFUNCT_1, BINOM;
definitions RLVECT_2, TARSKI;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RLSUB_1, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, STRUCT_0, PARTFUN1, RLVECT_3, INT_1, NUMBERS, NAT_1, XREAL_0, XXREAL_0, ENUMSET1, RLVECT_4, VFUNCT_1, BINOM, FUNCOP_1, FINSEQ_5, FUNCT_4, CARD_1;
schemes FINSEQ_1, NAT_1, FUNCT_2, RLVECT_4;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSET_1, NUMBERS, STRUCT_0, ORDINAL1, INT_1, XREAL_0, RLVECT_2, VALUED_0, FINSEQ_1, FINSEQ_2, CARD_1, NAT_1;
constructors HIDDEN, REALSET1, RLVECT_2, RLVECT_3, FUNCT_4, RUSUB_4, BINOP_2, FUNCSDOM, TOPREALB, VFUNCT_1, BINOM, REAL_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities RLVECT_2, RUSUB_4, FINSEQ_1;
expansions TARSKI, FINSEQ_1;
reconsider z0 = 0 as Real ;
deffunc H1( object ) -> Element of REAL = In (0,REAL);
Lm1:
for RS being RealLinearSpace
for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being INT -valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
Lm2:
for V being RealLinearSpace
for A being Subset of V
for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )