:: Vectors in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct RLSStruct  ->  addLoopStr ;
aggrRLSStruct(# carrier, ZeroF, addF, Mult #) ->  RLSStruct ;
sel Mult c1 ->  Function of [:REAL, the carrier of c1:], the carrier of c1;
end;

registration
cluster non empty for RLSStruct ;
existence
 not for b1 being RLSStruct holds b1 is empty
proofend;
end;

definition
let V be RLSStruct ;
mode VECTOR of V is Element of V;
end;

theorem :: RLVECT_1:1
for V being non empty 1-sorted
for v being Element of V holds v in V by STRUCT_0:def_5;

definition
let V be non empty RLSStruct ;
let v be VECTOR of V;
let a be real number ;
funca * v ->  Element of V equals :: RLVECT_1:def 1
 the Mult of V . (a,v);
coherence
 the Mult of V . (a,v) is Element of V
proofend;
end;

:: deftheorem  defines * RLVECT_1:def_1_:_
 for V being non empty RLSStruct
for v being VECTOR of V
for a being real number holds a * v = the Mult of V . (a,v);

:: Definitional theorems of zero element, addition, multiplication.
theorem :: RLVECT_1:2
for V being non empty addMagma
for v, w being Element of V holds v + w = the addF of V . (v,w) ;

registration
let ZS be non empty set ;
let O be Element of ZS;
let F be BinOp of ZS;
let G be Function of [:REAL,ZS:],ZS;
cluster RLSStruct(# ZS,O,F,G #) ->  non empty ;
coherence
 not RLSStruct(# ZS,O,F,G #) is empty ;
end;

definition
let IT be addMagma ;
attrIT is Abelian  means :Def2: :: RLVECT_1:def 2
 for v, w being Element of IT holds v + w = w + v;
attrIT is add-associative  means :Def3: :: RLVECT_1:def 3
 for u, v, w being Element of IT holds (u + v) + w = u + (v + w);
end;

:: deftheorem Def2 defines Abelian RLVECT_1:def_2_:_
 for IT being addMagma holds
( IT is Abelian iff for v, w being Element of IT holds v + w = w + v );

:: deftheorem Def3 defines add-associative RLVECT_1:def_3_:_
 for IT being addMagma holds
( IT is add-associative iff for u, v, w being Element of IT holds (u + v) + w = u + (v + w) );

definition
let IT be addLoopStr ;
attrIT is right_zeroed  means :Def4: :: RLVECT_1:def 4
 for v being Element of IT holds v + (0. IT) = v;
end;

:: deftheorem Def4 defines right_zeroed RLVECT_1:def_4_:_
 for IT being addLoopStr holds
( IT is right_zeroed iff for v being Element of IT holds v + (0. IT) = v );

definition
let IT be non empty RLSStruct ;
attrIT is vector-distributive  means :Def5: :: RLVECT_1:def 5
 for a being real number
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);
attrIT is scalar-distributive  means :Def6: :: RLVECT_1:def 6
 for a, b being real number
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);
attrIT is scalar-associative  means :Def7: :: RLVECT_1:def 7
 for a, b being real number
for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attrIT is scalar-unital  means :Def8: :: RLVECT_1:def 8
 for v being VECTOR of IT holds 1 * v = v;
end;

:: deftheorem Def5 defines vector-distributive RLVECT_1:def_5_:_
 for IT being non empty RLSStruct holds
( IT is vector-distributive iff for a being real number
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

:: deftheorem Def6 defines scalar-distributive RLVECT_1:def_6_:_
 for IT being non empty RLSStruct holds
( IT is scalar-distributive iff for a, b being real number
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

:: deftheorem Def7 defines scalar-associative RLVECT_1:def_7_:_
 for IT being non empty RLSStruct holds
( IT is scalar-associative iff for a, b being real number
for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

:: deftheorem Def8 defines scalar-unital RLVECT_1:def_8_:_
 for IT being non empty RLSStruct holds
( IT is scalar-unital iff for v being VECTOR of IT holds 1 * v = v );

definition
func Trivial-RLSStruct  ->  strict RLSStruct  equals :: RLVECT_1:def 9
 RLSStruct(# 1,op0,op2,(pr2 (REAL,1)) #);
coherence
 RLSStruct(# 1,op0,op2,(pr2 (REAL,1)) #) is strict RLSStruct ;
end;

:: deftheorem  defines Trivial-RLSStruct RLVECT_1:def_9_:_
 Trivial-RLSStruct = RLSStruct(# 1,op0,op2,(pr2 (REAL,1)) #);

registration
cluster Trivial-RLSStruct  -> 1 -element strict ;
coherence
 Trivial-RLSStruct is 1 -element
proofend;
end;

registration
cluster non empty strict Abelian add-associative for addMagma ;
existence
 ex b1 being addMagma st
( b1 is strict & b1 is Abelian & b1 is add-associative & not b1 is empty )
proofend;
end;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed for addLoopStr ;
existence
 ex b1 being addLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & not b1 is empty )
proofend;
end;

registration
cluster non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital for RLSStruct ;
existence
 ex b1 being non empty RLSStruct st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is scalar-distributive & b1 is vector-distributive & b1 is scalar-associative & b1 is scalar-unital )
proofend;
end;

definition
mode RealLinearSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
end;

definition
let V be Abelian addMagma ;
let v, w be Element of V;
:: original:+
redefine funcv + w ->  Element of the carrier of V;
commutativity
 for v, w being Element of V holds v + w = w + v by Def2;
end;

Lm1:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
proofend;

theorem Th3: :: RLVECT_1:3
for V being right_complementable add-associative right_zeroed addLoopStr holds V is right_add-cancelable
proofend;

theorem Th4: :: RLVECT_1:4
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( v + (0. V) = v & (0. V) + v = v )
proofend;

:: Definitions of reverse element to the vector and of
:: subtraction of vectors.
definition
let V be non empty addLoopStr ;
let v be Element of V;
assume A1: ( V is add-associative & V is right_zeroed & V is right_complementable ) ;
redefine func - v means :Def10: :: RLVECT_1:def 10
v + it = 0. V;
compatibility
 for b1 being Element of the carrier of V holds
( b1 = - v iff v + b1 = 0. V )
proofend;
end;

:: deftheorem Def10 defines - RLVECT_1:def_10_:_
 for V being non empty addLoopStr
for v being Element of V st V is add-associative & V is right_zeroed & V is right_complementable holds
for b3 being Element of the carrier of V holds
( b3 = - v iff v + b3 = 0. V );

Lm2:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V ex w being Element of V st v + w = u
proofend;

definition
let V be addLoopStr ;
let v, w be Element of V;
redefine func v - w equals :: RLVECT_1:def 11
v + (- w);
correctness
compatibility
for b1 being Element of the carrier of V holds
( b1 = v - w iff b1 = v + (- w) );
;
end;

:: deftheorem  defines - RLVECT_1:def_11_:_
 for V being addLoopStr
for v, w being Element of V holds v - w = v + (- w);

:: Definitional theorems of reverse element and substraction.
theorem Th5: :: RLVECT_1:5
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( v + (- v) = 0. V & (- v) + v = 0. V )
proofend;

theorem Th6: :: RLVECT_1:6
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v + w = 0. V holds
v = - w
proofend;

theorem :: RLVECT_1:7
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V ex w being Element of V st v + w = u by Lm2;

theorem Th8: :: RLVECT_1:8
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for w, u, v1, v2 being Element of V st ( w + v1 = w + v2 or v1 + w = v2 + w ) holds
v1 = v2
proofend;

theorem :: RLVECT_1:9
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st ( v + w = v or w + v = v ) holds
w = 0. V
proofend;

theorem Th10: :: RLVECT_1:10
for a being real number
for V being RealLinearSpace
for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
proofend;

theorem Th11: :: RLVECT_1:11
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
proofend;

theorem Th12: :: RLVECT_1:12
for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0. V) = 0. V
proofend;

theorem :: RLVECT_1:13
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds v - (0. V) = v
proofend;

theorem :: RLVECT_1:14
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds (0. V) - v = - v by Th4;

theorem :: RLVECT_1:15
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds v - v = 0. V by Def10;

theorem Th16: :: RLVECT_1:16
for V being RealLinearSpace
for v being VECTOR of V holds - v = (- 1) * v
proofend;

theorem Th17: :: RLVECT_1:17
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds - (- v) = v
proofend;

theorem Th18: :: RLVECT_1:18
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st - v = - w holds
v = w
proofend;

theorem Th19: :: RLVECT_1:19
for V being RealLinearSpace
for v being VECTOR of V st v = - v holds
v = 0. V
proofend;

theorem :: RLVECT_1:20
for V being RealLinearSpace
for v being VECTOR of V st v + v = 0. V holds
v = 0. V
proofend;

theorem Th21: :: RLVECT_1:21
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v - w = 0. V holds
v = w
proofend;

theorem :: RLVECT_1:22
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v being Element of V ex w being Element of V st v - w = u
proofend;

theorem :: RLVECT_1:23
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for w, v1, v2 being Element of V st w - v1 = w - v2 holds
v1 = v2
proofend;

theorem Th24: :: RLVECT_1:24
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds a * (- v) = (- a) * v
proofend;

theorem Th25: :: RLVECT_1:25
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds a * (- v) = - (a * v)
proofend;

theorem :: RLVECT_1:26
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds (- a) * (- v) = a * v
proofend;

Lm3:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, w being Element of V holds - (u + w) = (- w) + (- u)
proofend;

theorem Th27: :: RLVECT_1:27
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds v - (u + w) = (v - w) - u
proofend;

theorem :: RLVECT_1:28
for V being non empty add-associative addLoopStr
for v, u, w being Element of V holds (v + u) - w = v + (u - w) by Def3;

theorem :: RLVECT_1:29
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds v - (u - w) = (v - u) + w
proofend;

theorem Th30: :: RLVECT_1:30
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (v + w) = (- w) - v
proofend;

theorem Th31: :: RLVECT_1:31
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (v + w) = (- w) + (- v) by Lm3;

theorem :: RLVECT_1:32
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds (- v) - w = (- w) - v
proofend;

theorem :: RLVECT_1:33
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (v - w) = w + (- v)
proofend;

theorem Th34: :: RLVECT_1:34
for a being real number
for V being RealLinearSpace
for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
proofend;

theorem Th35: :: RLVECT_1:35
for a, b being real number
for V being RealLinearSpace
for v being VECTOR of V holds (a - b) * v = (a * v) - (b * v)
proofend;

theorem :: RLVECT_1:36
for a being real number
for V being RealLinearSpace
for v, w being VECTOR of V st a <> 0 &amp; a * v = a * w holds
v = w
proofend;

theorem :: RLVECT_1:37
for a, b being real number
for V being RealLinearSpace
for v being VECTOR of V st v <> 0. V &amp; a * v = b * v holds
a = b
proofend;

definition
let V be non empty addLoopStr ;
let F be the carrier of V -valued FinSequence;
func Sum F ->  Element of V means :Def12: :: RLVECT_1:def 12
 ex f being Function of NAT,V st
( it = f . (len F) &amp; f . 0 = 0. V &amp; ( for j being Element of NAT
for v being Element of V st j < len F &amp; v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );
existence
 ex b1 being Element of V ex f being Function of NAT,V st
( b1 = f . (len F) &amp; f . 0 = 0. V &amp; ( for j being Element of NAT
for v being Element of V st j < len F &amp; v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
proofend;
uniqueness
 for b1, b2 being Element of V st ex f being Function of NAT,V st
( b1 = f . (len F) &amp; f . 0 = 0. V &amp; ( for j being Element of NAT
for v being Element of V st j < len F &amp; v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) &amp; ex f being Function of NAT,V st
( b2 = f . (len F) &amp; f . 0 = 0. V &amp; ( for j being Element of NAT
for v being Element of V st j < len F &amp; v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines Sum RLVECT_1:def_12_:_
 for V being non empty addLoopStr
for F being the carrier of b1 -valued FinSequence
for b3 being Element of V holds
( b3 = Sum F iff ex f being Function of NAT,V st
( b3 = f . (len F) &amp; f . 0 = 0. V &amp; ( for j being Element of NAT
for v being Element of V st j < len F &amp; v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) );

Lm4:  for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
proofend;

Lm5:  for V being non empty addLoopStr
for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds
Sum F = 0. V
proofend;

theorem Th38: :: RLVECT_1:38
for V being non empty addLoopStr
for v being Element of V
for F, G being FinSequence of V st len F = (len G) + 1 &amp; G = F | (dom G) &amp; v = F . (len F) holds
Sum F = (Sum G) + v
proofend;

theorem :: RLVECT_1:39
for a being real number
for V being RealLinearSpace
for F, G being FinSequence of V st len F = len G &amp; ( for k being Element of NAT
for v being VECTOR of V st k in dom F &amp; v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proofend;

theorem :: RLVECT_1:40
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of V st len F = len G &amp; ( for k being Element of NAT
for v being Element of V st k in dom F &amp; v = G . k holds
F . k = - v ) holds
Sum F = - (Sum G)
proofend;

theorem Th41: :: RLVECT_1:41
for V being non empty add-associative right_zeroed addLoopStr
for F, G being FinSequence of V holds Sum (F ^ G) = (Sum F) + (Sum G)
proofend;

Lm6:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v
proofend;

theorem :: RLVECT_1:42
for V being non empty Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of V st rng F = rng G &amp; F is one-to-one &amp; G is one-to-one holds
Sum F = Sum G
proofend;

theorem Th43: :: RLVECT_1:43
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V by Lm4;

theorem :: RLVECT_1:44
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v by Lm6;

theorem Th45: :: RLVECT_1:45
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V holds Sum <*v,u*> = v + u
proofend;

theorem Th46: :: RLVECT_1:46
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*v,u,w*> = (v + u) + w
proofend;

theorem :: RLVECT_1:47
for V being RealLinearSpace
for a being Real holds a * (Sum (<*> the carrier of V)) = 0. V by Lm4, Th10;

theorem :: RLVECT_1:48
for V being RealLinearSpace
for a being Real
for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
proofend;

theorem :: RLVECT_1:49
for V being RealLinearSpace
for a being Real
for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
proofend;

theorem :: RLVECT_1:50
for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V
proofend;

theorem :: RLVECT_1:51
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds - (Sum <*v*>) = - v by Lm6;

theorem :: RLVECT_1:52
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u
proofend;

theorem :: RLVECT_1:53
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w
proofend;

theorem Th54: :: RLVECT_1:54
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*v,w*> = Sum <*w,v*>
proofend;

theorem :: RLVECT_1:55
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)
proofend;

theorem :: RLVECT_1:56
canceled;

theorem :: RLVECT_1:57
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( Sum <*(0. V),v*> = v &amp; Sum <*v,(0. V)*> = v )
proofend;

theorem :: RLVECT_1:58
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( Sum <*v,(- v)*> = 0. V &amp; Sum <*(- v),v*> = 0. V )
proofend;

theorem :: RLVECT_1:59
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*v,(- w)*> = v - w by Th45;

theorem Th60: :: RLVECT_1:60
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*(- v),(- w)*> = - (w + v)
proofend;

theorem Th61: :: RLVECT_1:61
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v*> = 2 * v
proofend;

theorem :: RLVECT_1:62
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- 2) * v
proofend;

theorem :: RLVECT_1:63
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v, w being Element of V holds Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)
proofend;

theorem :: RLVECT_1:64
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,v*>) + w
proofend;

theorem :: RLVECT_1:65
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*v,w*>) + u
proofend;

theorem Th66: :: RLVECT_1:66
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,w*>) + v
proofend;

theorem Th67: :: RLVECT_1:67
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*u,w,v*>
proofend;

theorem Th68: :: RLVECT_1:68
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,u,w*>
proofend;

theorem Th69: :: RLVECT_1:69
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,w,u*>
proofend;

theorem :: RLVECT_1:70
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*w,v,u*>
proofend;

theorem :: RLVECT_1:71
canceled;

theorem :: RLVECT_1:72
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( Sum <*(0. V),(0. V),v*> = v &amp; Sum <*(0. V),v,(0. V)*> = v &amp; Sum <*v,(0. V),(0. V)*> = v )
proofend;

theorem :: RLVECT_1:73
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v being Element of V holds
( Sum <*(0. V),u,v*> = u + v &amp; Sum <*u,v,(0. V)*> = u + v &amp; Sum <*u,(0. V),v*> = u + v )
proofend;

theorem :: RLVECT_1:74
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v,v*> = 3 * v
proofend;

theorem :: RLVECT_1:75
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V st len F = 0 holds
Sum F = 0. V by Lm5;

theorem :: RLVECT_1:76
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V st len F = 1 holds
Sum F = F . 1
proofend;

theorem :: RLVECT_1:77
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V
for v1, v2 being Element of V st len F = 2 &amp; v1 = F . 1 &amp; v2 = F . 2 holds
Sum F = v1 + v2
proofend;

theorem :: RLVECT_1:78
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V
for v1, v2, v being Element of V st len F = 3 &amp; v1 = F . 1 &amp; v2 = F . 2 &amp; v = F . 3 holds
Sum F = (v1 + v2) + v
proofend;

begin

definition
let L be non empty addLoopStr ;
attrL is zeroed  means :Def13: :: RLVECT_1:def 13
 for a being Element of L holds
( a + (0. L) = a &amp; (0. L) + a = a );
end;

:: deftheorem Def13 defines zeroed RLVECT_1:def_13_:_
 for L being non empty addLoopStr holds
( L is zeroed iff for a being Element of L holds
( a + (0. L) = a &amp; (0. L) + a = a ) );

registration
cluster non empty zeroed  ->  non empty right_zeroed for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is zeroed holds
b1 is right_zeroed
proofend;
end;

registration
cluster non empty Abelian right_zeroed  ->  non empty zeroed for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Abelian &amp; b1 is right_zeroed holds
b1 is zeroed
proofend;
cluster non empty right_complementable Abelian  ->  non empty left_complementable for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Abelian &amp; b1 is right_complementable holds
b1 is left_complementable
proofend;
end;

theorem :: RLVECT_1:79
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds (- a) * v = - (a * v)
proofend;

begin

theorem :: RLVECT_1:80
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V
proofend;

theorem :: RLVECT_1:81
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u
proofend;

theorem :: RLVECT_1:82
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w
proofend;

theorem :: RLVECT_1:83
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v being Element of V holds
( Sum <*v,(- v)*> = 0. V &amp; Sum <*(- v),v*> = 0. V )
proofend;

theorem :: RLVECT_1:84
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds
( Sum <*v,(- w)*> = v - w &amp; Sum <*(- w),v*> = v - w )
proofend;

theorem :: RLVECT_1:85
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds
( Sum <*(- v),(- w)*> = - (v + w) &amp; Sum <*(- w),(- v)*> = - (v + w) )
proofend;