begin
reconsider z0 = 0 as Real ;
deffunc H1( set ) -> Element of NAT = 0 ;
theorem
theorem
theorem Th3:
begin
:: deftheorem Def1 defines * RLVECT_X:def 1 :
for V being RealLinearSpace
for i being Integer
for L, b4 being Linear_Combination of V holds
( b4 = i * L iff for v being VECTOR of V holds b4 . v = i * (L . v) );
:: deftheorem defines Z_Lin RLVECT_X:def 2 :
for V being RealLinearSpace
for A being Subset of V holds Z_Lin A = { (Sum l) where l is Linear_Combination of A : rng l c= INT } ;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem Th16:
theorem
theorem
theorem Th19:
theorem
theorem
theorem Th22:
theorem
theorem
Lm1:
for RS being RealLinearSpace
for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being integer-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 integer-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) ) )
theorem
:: deftheorem defines Z_Lin RLVECT_X:def 3 :
for RS being RealLinearSpace
for f being FinSequence of RS holds Z_Lin f = { (Sum g) where g is len b2 -element FinSequence of RS : ex a being len b2 -element integer-valued FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } ;
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
theorem