:: RLVECT_1 semantic presentation

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
proof
set ZS = the non empty set ;
set O = the Element of the non empty set ;
set F = the BinOp of the non empty set ;
set G = the Function of [:REAL, the non empty set :], the non empty set ;
take  RLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) ; ::_thesis: not RLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty
thus  not the carrier of RLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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
proof
reconsider a = a as Real by XREAL_0:def_1;
 the Mult of V . (a,v) is Element of V ;
hence  the Mult of V . (a,v) is Element of V ; ::_thesis: verum
end;
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);

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
proof
 the carrier of Trivial-RLSStruct = {{}} by CARD_1:49;
hence  the carrier of Trivial-RLSStruct is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
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 )
proof
take S = Trivial-addMagma ; ::_thesis: ( S is strict & S is Abelian & S is add-associative & not S is empty )
thus  S is strict ; ::_thesis: ( S is Abelian & S is add-associative & not S is empty )
thus  S is Abelian ::_thesis: ( S is add-associative & not S is empty )
proof
let x be Element of S; :: according to RLVECT_1:def_2 ::_thesis: for w being Element of S holds x + w = w + x
thus  for w being Element of S holds x + w = w + x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is add-associative ::_thesis: not S is empty
proof
let x be Element of S; :: according to RLVECT_1:def_3 ::_thesis: for v, w being Element of S holds (x + v) + w = x + (v + w)
thus  for v, w being Element of S holds (x + v) + w = x + (v + w) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  not S is empty ; ::_thesis: verum
end;
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 )
proof
take S = Trivial-addLoopStr ; ::_thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
thus  S is strict ; ::_thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
thus  S is Abelian ::_thesis: ( S is add-associative & S is right_zeroed & S is right_complementable & not S is empty )
proof
let x be Element of S; :: according to RLVECT_1:def_2 ::_thesis: for w being Element of S holds x + w = w + x
thus  for w being Element of S holds x + w = w + x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is add-associative ::_thesis: ( S is right_zeroed & S is right_complementable & not S is empty )
proof
let x be Element of S; :: according to RLVECT_1:def_3 ::_thesis: for v, w being Element of S holds (x + v) + w = x + (v + w)
thus  for v, w being Element of S holds (x + v) + w = x + (v + w) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is right_zeroed ::_thesis: ( S is right_complementable & not S is empty )
proof
let x be Element of S; :: according to RLVECT_1:def_4 ::_thesis: x + (0. S) = x
thus  x + (0. S) = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  ( S is right_complementable & not S is empty ) ; ::_thesis: verum
end;
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 )
proof
take S = Trivial-RLSStruct ; ::_thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus  S is strict ; ::_thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus  S is Abelian ::_thesis: ( S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_2 ::_thesis: for w being Element of S holds x + w = w + x
thus  for w being Element of S holds x + w = w + x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is add-associative ::_thesis: ( S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_3 ::_thesis: for v, w being Element of S holds (x + v) + w = x + (v + w)
thus  for v, w being Element of S holds (x + v) + w = x + (v + w) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is right_zeroed ::_thesis: ( S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_4 ::_thesis: x + (0. S) = x
thus  x + (0. S) = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is right_complementable ::_thesis: ( S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take  x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. S
thus  x + x = 0. S by STRUCT_0:def_10; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of S holds (a + b) * v = (a * v) + (b * v) by STRUCT_0:def_10; :: according to RLVECT_1:def_6 ::_thesis: ( S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus  for a being real number
for v, w being VECTOR of S holds a * (v + w) = (a * v) + (a * w) by STRUCT_0:def_10; :: according to RLVECT_1:def_5 ::_thesis: ( S is scalar-associative & S is scalar-unital )
thus  for a, b being real number
for v being VECTOR of S holds (a * b) * v = a * (b * v) by STRUCT_0:def_10; :: according to RLVECT_1:def_7 ::_thesis: S is scalar-unital
thus  for v being VECTOR of S holds 1 * v = v by STRUCT_0:def_10; :: according to RLVECT_1:def_8 ::_thesis: verum
end;
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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
let v, w be Element of V; ::_thesis: ( v + w = 0. V implies w + v = 0. V )
assume A1: v + w = 0. V ; ::_thesis: w + v = 0. V
consider u being Element of V such that
A2: w + u = 0. V by ALGSTR_0:def_11;
w + v = w + (v + (w + u)) by A2, Def4
.= w + ((v + w) + u) by Def3
.= (w + (v + w)) + u by Def3
.= w + u by A1, Def4 ;
hence  w + v = 0. V by A2; ::_thesis: verum
end;

theorem Th3: :: RLVECT_1:3
for V being right_complementable add-associative right_zeroed addLoopStr holds V is right_add-cancelable
proof
let V be right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: V is right_add-cancelable
let v be Element of V; :: according to ALGSTR_0:def_7 ::_thesis: v is right_add-cancelable
consider v1 being Element of V such that
A1: v + v1 = 0. V by ALGSTR_0:def_11;
let u, w be Element of V; :: according to ALGSTR_0:def_4 ::_thesis: ( not u + v = w + v or u = w )
assume A2: u + v = w + v ; ::_thesis: u = w
thus u = u + (0. V) by Def4
.= (u + v) + v1 by A1, Def3
.= w + (0. V) by A1, A2, Def3
.= w by Def4 ; ::_thesis: verum
end;

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 )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( v + (0. V) = v & (0. V) + v = v )
let v be Element of V; ::_thesis: ( v + (0. V) = v & (0. V) + v = v )
consider w being Element of V such that
A1: v + w = 0. V by ALGSTR_0:def_11;
thus A2: v + (0. V) = v by Def4; ::_thesis: (0. V) + v = v
 w + v = 0. V by A1, Lm1;
hence  (0. V) + v = v by A2, A1, Def3; ::_thesis: verum
end;

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 )
proof
let IT be Element of V; ::_thesis: ( IT = - v iff v + IT = 0. V )
consider v1 being Element of V such that
A2: v + v1 = 0. V by A1, ALGSTR_0:def_11;
A3: V is right_add-cancelable by A1, Th3;
A4: v is left_complementable
proof
take  v1 ; :: according to ALGSTR_0:def_10 ::_thesis: v1 + v = 0. V
(v1 + v) + v1 = v1 + (0. V) by A1, A2, Def3
.= v1 by A1, Th4
.= (0. V) + v1 by A1, Th4 ;
hence  v1 + v = 0. V by A3, ALGSTR_0:def_4; ::_thesis: verum
end;
(v + (- v)) + v = v + ((- v) + v) by A1, Def3
.= v + (0. V) by A3, A4, ALGSTR_0:def_13
.= v by A1, Th4
.= (0. V) + v by A1, Th4 ;
hence  ( IT = - v implies v + IT = 0. V ) by A3, ALGSTR_0:def_4; ::_thesis: ( v + IT = 0. V implies IT = - v )
assume A5: v + IT = 0. V ; ::_thesis: IT = - v
thus IT = (0. V) + IT by A1, Th4
.= ((- v) + v) + IT by A3, A4, ALGSTR_0:def_13
.= (- v) + (0. V) by A1, A5, Def3
.= - v by A1, Th4 ; ::_thesis: verum
end;
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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V ex w being Element of V st v + w = u
let v, u be Element of V; ::_thesis: ex w being Element of V st v + w = u
take w = (- v) + u; ::_thesis: v + w = u
thus v + w = (v + (- v)) + u by Def3
.= (0. V) + u by Def10
.= u by Th4 ; ::_thesis: verum
end;

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);

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 )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( v + (- v) = 0. V & (- v) + v = 0. V )
let v be Element of V; ::_thesis: ( v + (- v) = 0. V & (- v) + v = 0. V )
thus  v + (- v) = 0. V by Def10; ::_thesis: (- v) + v = 0. V
hence  (- v) + v = 0. V by Lm1; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V st v + w = 0. V holds
v = - w
let v, w be Element of V; ::_thesis: ( v + w = 0. V implies v = - w )
assume  v + w = 0. V ; ::_thesis: v = - w
then  w + v = 0. V by Lm1;
hence  v = - w by Def10; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w, u, v1, v2 being Element of V st ( w + v1 = w + v2 or v1 + w = v2 + w ) holds
v1 = v2
let w, u, v1, v2 be Element of V; ::_thesis: ( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 )
A1: now__::_thesis:_(_v1_+_w_=_v2_+_w_implies_v1_=_v2_)
assume A2: v1 + w = v2 + w ; ::_thesis: v1 = v2
thus v1 = v1 + (0. V) by Th4
.= v1 + (w + (- w)) by Th5
.= (v1 + w) + (- w) by Def3
.= v2 + (w + (- w)) by A2, Def3
.= v2 + (0. V) by Th5
.= v2 by Th4 ; ::_thesis: verum
end;
now__::_thesis:_(_w_+_v1_=_w_+_v2_implies_v1_=_v2_)
assume A3: w + v1 = w + v2 ; ::_thesis: v1 = v2
thus v1 = (0. V) + v1 by Th4
.= ((- w) + w) + v1 by Th5
.= (- w) + (w + v1) by Def3
.= ((- w) + w) + v2 by A3, Def3
.= (0. V) + v2 by Th5
.= v2 by Th4 ; ::_thesis: verum
end;
hence  ( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 ) by A1; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V st ( v + w = v or w + v = v ) holds
w = 0. V
let v, w be Element of V; ::_thesis: ( ( v + w = v or w + v = v ) implies w = 0. V )
assume  ( v + w = v or w + v = v ) ; ::_thesis: w = 0. V
then  ( v + w = v + (0. V) or w + v = (0. V) + v ) by Th4;
hence  w = 0. V by Th8; ::_thesis: verum
end;

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
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let v be VECTOR of V; ::_thesis: ( ( a = 0 or v = 0. V ) implies a * v = 0. V )
assume A1: ( a = 0 or v = 0. V ) ; ::_thesis: a * v = 0. V
now__::_thesis:_a_*_v_=_0._V
percases ( a = 0 or v = 0. V ) by A1;
supposeA2: a = 0 ; ::_thesis: a * v = 0. V
v + (0 * v) = (1 * v) + (0 * v) by Def8
.= (1 + 0) * v by Def6
.= v by Def8
.= v + (0. V) by Th4 ;
hence  a * v = 0. V by A2, Th8; ::_thesis: verum
end;
supposeA3: v = 0. V ; ::_thesis: a * v = 0. V
(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by Def5
.= a * (0. V) by Th4
.= (a * (0. V)) + (0. V) by Th4 ;
hence  a * v = 0. V by A3, Th8; ::_thesis: verum
end;
end;
end;
hence  a * v = 0. V ; ::_thesis: verum
end;

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 )
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let v be VECTOR of V; ::_thesis: ( not a * v = 0. V or a = 0 or v = 0. V )
assume that
A1: a * v = 0. V and
A2: a <> 0 ; ::_thesis: v = 0. V
thus v = 1 * v by Def8
.= ((a ") * a) * v by A2, XCMPLX_0:def_7
.= (a ") * (0. V) by A1, Def7
.= 0. V by Th10 ; ::_thesis: verum
end;

theorem Th12: :: RLVECT_1:12
for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0. V) = 0. V
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: - (0. V) = 0. V
thus  0. V = (0. V) + (- (0. V)) by Def10
.= - (0. V) by Th4 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds v - (0. V) = v
let v be Element of V; ::_thesis: v - (0. V) = v
thus v - (0. V) = v + (0. V) by Th12
.= v by Th4 ; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds - v = (- 1) * v
let v be VECTOR of V; ::_thesis: - v = (- 1) * v
v + ((- 1) * v) = (1 * v) + ((- 1) * v) by Def8
.= (1 + (- 1)) * v by Def6
.= 0. V by Th10 ;
hence  - v = (- v) + (v + ((- 1) * v)) by Th4
.= ((- v) + v) + ((- 1) * v) by Def3
.= (0. V) + ((- 1) * v) by Def10
.= (- 1) * v by Th4 ;
::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds - (- v) = v
let v be Element of V; ::_thesis: - (- v) = v
 v + (- v) = 0. V by Def10;
hence  - (- v) = v by Th6; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V st - v = - w holds
v = w
let v, w be Element of V; ::_thesis: ( - v = - w implies v = w )
assume  - v = - w ; ::_thesis: v = w
hence v = - (- w) by Th17
.= w by Th17 ;
::_thesis: verum
end;

theorem Th19: :: RLVECT_1:19
for V being RealLinearSpace
for v being VECTOR of V st v = - v holds
v = 0. V
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st v = - v holds
v = 0. V
let v be VECTOR of V; ::_thesis: ( v = - v implies v = 0. V )
assume  v = - v ; ::_thesis: v = 0. V
then  0. V = v + v by Def10
.= (1 * v) + v by Def8
.= (1 * v) + (1 * v) by Def8
.= (1 + 1) * v by Def6
.= 2 * v ;
hence  v = 0. V by Th11; ::_thesis: verum
end;

theorem :: RLVECT_1:20
for V being RealLinearSpace
for v being VECTOR of V st v + v = 0. V holds
v = 0. V
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st v + v = 0. V holds
v = 0. V
let v be VECTOR of V; ::_thesis: ( v + v = 0. V implies v = 0. V )
assume  v + v = 0. V ; ::_thesis: v = 0. V
then  v = - v by Def10;
hence  v = 0. V by Th19; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V st v - w = 0. V holds
v = w
let v, w be Element of V; ::_thesis: ( v - w = 0. V implies v = w )
assume  v - w = 0. V ; ::_thesis: v = w
then  - v = - w by Def10;
hence  v = w by Th18; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for u, v being Element of V ex w being Element of V st v - w = u
let u, v be Element of V; ::_thesis: ex w being Element of V st v - w = u
consider w being Element of V such that
A1: v + w = u by Lm2;
take  - w ; ::_thesis: v - (- w) = u
thus  v - (- w) = u by A1, Th17; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w, v1, v2 being Element of V st w - v1 = w - v2 holds
v1 = v2
let w, v1, v2 be Element of V; ::_thesis: ( w - v1 = w - v2 implies v1 = v2 )
assume  w - v1 = w - v2 ; ::_thesis: v1 = v2
then  - v1 = - v2 by Th8;
hence  v1 = v2 by Th18; ::_thesis: verum
end;

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
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds a * (- v) = (- a) * v
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds a * (- v) = (- a) * v
let v be VECTOR of V; ::_thesis: a * (- v) = (- a) * v
thus a * (- v) = a * ((- 1) * v) by Th16
.= (a * (- 1)) * v by Def7
.= (- a) * v ; ::_thesis: verum
end;

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)
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds a * (- v) = - (a * v)
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds a * (- v) = - (a * v)
let v be VECTOR of V; ::_thesis: a * (- v) = - (a * v)
thus a * (- v) = (- (1 * a)) * v by Th24
.= ((- 1) * a) * v
.= (- 1) * (a * v) by Def7
.= - (a * v) by Th16 ; ::_thesis: verum
end;

theorem :: RLVECT_1:26
for a being real number
for V being RealLinearSpace
for v being VECTOR of V holds (- a) * (- v) = a * v
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds (- a) * (- v) = a * v
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds (- a) * (- v) = a * v
let v be VECTOR of V; ::_thesis: (- a) * (- v) = a * v
thus (- a) * (- v) = (- (- a)) * v by Th24
.= a * v ; ::_thesis: verum
end;

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)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for u, w being Element of V holds - (u + w) = (- w) + (- u)
let u, w be Element of V; ::_thesis: - (u + w) = (- w) + (- u)
(u + w) + ((- w) + (- u)) = u + (w + ((- w) + (- u))) by Def3
.= u + ((w + (- w)) + (- u)) by Def3
.= u + ((0. V) + (- u)) by Def10
.= u + (- u) by Th4
.= 0. V by Def10 ;
hence  - (u + w) = (- w) + (- u) by Def10; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds v - (u + w) = (v - w) - u
let v, u, w be Element of V; ::_thesis: v - (u + w) = (v - w) - u
thus v - (u + w) = v + ((- w) + (- u)) by Lm3
.= (v - w) - u by Def3 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds v - (u - w) = (v - u) + w
let v, u, w be Element of V; ::_thesis: v - (u - w) = (v - u) + w
thus v - (u - w) = v - (u + (- w))
.= (v - u) - (- w) by Th27
.= (v - u) + w by Th17 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds - (v + w) = (- w) - v
let v, w be Element of V; ::_thesis: - (v + w) = (- w) - v
thus  - (v + w) = (0. V) - (v + w) by Th4
.= ((0. V) - w) - v by Th27
.= (- w) - v by Th4 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds (- v) - w = (- w) - v
let v, w be Element of V; ::_thesis: (- v) - w = (- w) - v
thus (- v) - w = - (w + v) by Th30
.= (- w) - v by Th30 ; ::_thesis: verum
end;

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)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds - (v - w) = w + (- v)
let v, w be Element of V; ::_thesis: - (v - w) = w + (- v)
thus  - (v - w) = (- (- w)) + (- v) by Lm3
.= w + (- v) by Th17 ; ::_thesis: verum
end;

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)
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
let v, w be VECTOR of V; ::_thesis: a * (v - w) = (a * v) - (a * w)
thus a * (v - w) = (a * v) + (a * (- w)) by Def5
.= (a * v) - (a * w) by Th25 ; ::_thesis: verum
end;

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)
proof
let a, b be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds (a - b) * v = (a * v) - (b * v)
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds (a - b) * v = (a * v) - (b * v)
let v be VECTOR of V; ::_thesis: (a - b) * v = (a * v) - (b * v)
thus (a - b) * v = (a + (- b)) * v
.= (a * v) + ((- b) * v) by Def6
.= (a * v) + (b * (- v)) by Th24
.= (a * v) - (b * v) by Th25 ; ::_thesis: verum
end;

theorem :: RLVECT_1:36
for a being real number
for V being RealLinearSpace
for v, w being VECTOR of V st a <> 0 & a * v = a * w holds
v = w
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V st a <> 0 & a * v = a * w holds
v = w
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V st a <> 0 & a * v = a * w holds
v = w
let v, w be VECTOR of V; ::_thesis: ( a <> 0 & a * v = a * w implies v = w )
assume that
A1: a <> 0 and
A2: a * v = a * w ; ::_thesis: v = w
0. V = (a * v) - (a * w) by A2, Def10
.= a * (v - w) by Th34 ;
then  v - w = 0. V by A1, Th11;
hence  v = w by Th21; ::_thesis: verum
end;

theorem :: RLVECT_1:37
for a, b being real number
for V being RealLinearSpace
for v being VECTOR of V st v <> 0. V & a * v = b * v holds
a = b
proof
let a, b be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V st v <> 0. V & a * v = b * v holds
a = b
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st v <> 0. V & a * v = b * v holds
a = b
let v be VECTOR of V; ::_thesis: ( v <> 0. V & a * v = b * v implies a = b )
assume that
A1: v <> 0. V and
A2: a * v = b * v ; ::_thesis: a = b
0. V = (a * v) - (b * v) by A2, Def10
.= (a - b) * v by Th35 ;
then  (- b) + a = 0 by A1, Th11;
hence  a = b ; ::_thesis: verum
end;


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) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & 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) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
proof
defpred S1[ set ] means  for F being the carrier of V -valued FinSequence st len F = $1 holds
ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for F being the carrier of V -valued FinSequence st len F = n holds
ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ; ::_thesis: S1[n + 1]
let F be the carrier of V -valued FinSequence; ::_thesis: ( len F = n + 1 implies ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) )
A3: rng F c= the carrier of V by RELAT_1:def_19;
then reconsider F1 = F as FinSequence of V by FINSEQ_1:def_4;
reconsider G = F1 | (Seg n) as FinSequence of V by FINSEQ_1:18;
assume A4: len F = n + 1 ; ::_thesis: ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
then  dom F = Seg (n + 1) by FINSEQ_1:def_3;
then  n + 1 in dom F by FINSEQ_1:4;
then  F . (n + 1) in rng F by FUNCT_1:def_3;
then reconsider u1 = F . (n + 1) as Element of V by A3;
A5: n < n + 1 by NAT_1:13;
then consider u being Element of V, f being Function of NAT,V such that
 u = f . (len G) and
A6: f . 0 = 0. V and
A7: for j being Element of NAT
for v being Element of V st j < len G & v = G . (j + 1) holds
f . (j + 1) = (f . j) + v by A2, A4, FINSEQ_1:17;
defpred S2[ set , set ] means  for j being Element of NAT st $1 = j holds
( ( j < n + 1 implies $2 = f . $1 ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
$2 = (f . (len G)) + u ) );
A8: for k being Element of NAT ex v being Element of V st S2[k,v]
proof
let k be Element of NAT ; ::_thesis: ex v being Element of V st S2[k,v]
reconsider i = k as Element of NAT ;
A9: now__::_thesis:_(_n_+_1_<=_i_implies_ex_v_being_Element_of_the_carrier_of_V_st_
for_j_being_Element_of_NAT_st_k_=_j_holds_
(_(_j_<_n_+_1_implies_v_=_f_._k_)_&_(_n_+_1_<=_j_implies_for_u2_being_Element_of_V_st_u2_=_F_._(n_+_1)_holds_
v_=_(f_._(len_G))_+_u2_)_)_)
assume A10: n + 1 <= i ; ::_thesis: ex v being Element of the carrier of V st
for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )
take v = (f . (len G)) + u1; ::_thesis: for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )
let j be Element of NAT ; ::_thesis: ( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) ) )
assume  k = j ; ::_thesis: ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )
hence  ( j < n + 1 implies v = f . k ) by A10; ::_thesis: ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 )
assume  n + 1 <= j ; ::_thesis: for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2
let u2 be Element of V; ::_thesis: ( u2 = F . (n + 1) implies v = (f . (len G)) + u2 )
assume  u2 = F . (n + 1) ; ::_thesis: v = (f . (len G)) + u2
hence  v = (f . (len G)) + u2 ; ::_thesis: verum
end;
now__::_thesis:_(_i_<_n_+_1_implies_ex_v_being_Element_of_the_carrier_of_V_st_
for_j_being_Element_of_NAT_st_k_=_j_holds_
(_(_j_<_n_+_1_implies_v_=_f_._k_)_&_(_n_+_1_<=_j_implies_for_u_being_Element_of_V_st_u_=_F_._(n_+_1)_holds_
v_=_(f_._(len_G))_+_u_)_)_)
assume A11: i < n + 1 ; ::_thesis: ex v being Element of the carrier of V st
for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )
take v = f . k; ::_thesis: for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )
let j be Element of NAT ; ::_thesis: ( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) ) )
assume A12: k = j ; ::_thesis: ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )
thus  ( j < n + 1 implies v = f . k ) ; ::_thesis: ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u )
thus  ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) by A11, A12; ::_thesis: verum
end;
hence  ex v being Element of V st S2[k,v] by A9; ::_thesis: verum
end;
consider f9 being Function of NAT, the carrier of V such that
A13: for k being Element of NAT holds S2[k,f9 . k] from FUNCT_2:sch_3(A8);
take z = f9 . (n + 1); ::_thesis: ex f being Function of NAT,V st
( z = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
take f99 = f9; ::_thesis: ( z = f99 . (len F) & f99 . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v ) )
thus  z = f99 . (len F) by A4; ::_thesis: ( f99 . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v ) )
thus  f99 . 0 = 0. V by A6, A13; ::_thesis: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v
let j be Element of NAT ; ::_thesis: for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v
let v be Element of V; ::_thesis: ( j < len F & v = F . (j + 1) implies f99 . (j + 1) = (f99 . j) + v )
assume that
A14: j < len F and
A15: v = F . (j + 1) ; ::_thesis: f99 . (j + 1) = (f99 . j) + v
A16: len G = n by A4, A5, FINSEQ_1:17;
A17: now__::_thesis:_(_j_=_n_implies_f99_._(j_+_1)_=_(f99_._j)_+_v_)
assume A18: j = n ; ::_thesis: f99 . (j + 1) = (f99 . j) + v
then  f99 . (j + 1) = (f . j) + v by A16, A13, A15;
hence  f99 . (j + 1) = (f99 . j) + v by A5, A13, A18; ::_thesis: verum
end;
A19: now__::_thesis:_(_j_<_n_implies_f99_._(j_+_1)_=_(f99_._j)_+_v_)
assume A20: j < n ; ::_thesis: f99 . (j + 1) = (f99 . j) + v
then A21: j + 1 < n + 1 by XREAL_1:6;
 ( 1 <= 1 + j & j + 1 <= n ) by A20, NAT_1:11, NAT_1:13;
then  j + 1 in Seg n by FINSEQ_1:1;
then A22: v = G . (j + 1) by A15, FUNCT_1:49;
 j < len G by A4, A5, A20, FINSEQ_1:17;
then A23: f . (j + 1) = (f . j) + v by A7, A22;
 j < n + 1 by A20, NAT_1:13;
then  f . (j + 1) = (f9 . j) + v by A13, A23;
hence  f99 . (j + 1) = (f99 . j) + v by A13, A21; ::_thesis: verum
end;
 j <= n by A4, A14, NAT_1:13;
hence  f99 . (j + 1) = (f99 . j) + v by A19, A17, XXREAL_0:1; ::_thesis: verum
end;
A24: S1[ 0 ]
proof
reconsider f = NAT --> (0. V) as Function of NAT, the carrier of V ;
let F be the carrier of V -valued FinSequence; ::_thesis: ( len F = 0 implies ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) )
assume A25: len F = 0 ; ::_thesis: ex u being Element of V ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
take u = f . (len F); ::_thesis: ex f being Function of NAT,V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
take f9 = f; ::_thesis: ( u = f9 . (len F) & f9 . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v ) )
thus  ( u = f9 . (len F) & f9 . 0 = 0. V ) by FUNCOP_1:7; ::_thesis: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v
let j be Element of NAT ; ::_thesis: for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v
thus  for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v by A25; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A24, A1);
hence  ex b1 being Element of V ex f being Function of NAT,V st
( b1 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of V st ex f being Function of NAT,V st
( b1 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) & ex f being Function of NAT,V st
( b2 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) holds
b1 = b2
proof
let v1, v2 be Element of V; ::_thesis: ( ex f being Function of NAT,V st
( v1 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) & ex f being Function of NAT,V st
( v2 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) implies v1 = v2 )
given f being Function of NAT,V such that A26: v1 = f . (len F) and
A27: f . 0 = 0. V and
A28: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ; ::_thesis: ( for f being Function of NAT,V holds
( not v2 = f . (len F) or not f . 0 = 0. V or ex j being Element of NAT ex v being Element of V st
( j < len F & v = F . (j + 1) & not f . (j + 1) = (f . j) + v ) ) or v1 = v2 )
given f9 being Function of NAT,V such that A29: v2 = f9 . (len F) and
A30: f9 . 0 = 0. V and
A31: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v ; ::_thesis: v1 = v2
defpred S1[ Element of NAT ] means ( $1 <= len F implies f . $1 = f9 . $1 );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_len_F_implies_f_._k_=_f9_._k_)_&_k_+_1_<=_len_F_holds_
f_._(k_+_1)_=_f9_._(k_+_1)
A32: rng F c= the carrier of V by RELAT_1:def_19;
let k be Element of NAT ; ::_thesis: ( ( k <= len F implies f . k = f9 . k ) & k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A33: ( k <= len F implies f . k = f9 . k ) ; ::_thesis: ( k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A34: k + 1 <= len F ; ::_thesis: f . (k + 1) = f9 . (k + 1)
 ( 1 <= k + 1 & dom F = Seg (len F) ) by FINSEQ_1:def_3, NAT_1:11;
then  k + 1 in dom F by A34, FINSEQ_1:1;
then  F . (k + 1) in rng F by FUNCT_1:def_3;
then reconsider u1 = F . (k + 1) as Element of V by A32;
A35: k < len F by A34, NAT_1:13;
then  f . (k + 1) = (f . k) + u1 by A28;
hence  f . (k + 1) = f9 . (k + 1) by A31, A33, A35; ::_thesis: verum
end;
then A36: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A37: S1[ 0 ] by A27, A30;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A37, A36);
hence  v1 = v2 by A26, A29; ::_thesis: verum
end;
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) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & 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
proof
let V be non empty addLoopStr ; ::_thesis: Sum (<*> the carrier of V) = 0. V
set S = <*> the carrier of V;
 ex f being Function of NAT,V st
( Sum (<*> the carrier of V) = f . (len (<*> the carrier of V)) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len (<*> the carrier of V) & v = (<*> the carrier of V) . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by Def12;
hence  Sum (<*> the carrier of V) = 0. V ; ::_thesis: verum
end;

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
proof
let V be non empty addLoopStr ; ::_thesis: for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds
Sum F = 0. V
let F be FinSequence-like PartFunc of NAT,V; ::_thesis: ( len F = 0 implies Sum F = 0. V )
assume  len F = 0 ; ::_thesis: Sum F = 0. V
then  F = <*> the carrier of V ;
hence  Sum F = 0. V by Lm4; ::_thesis: verum
end;

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 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
proof
let V be non empty addLoopStr ; ::_thesis: for v being Element of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
let v be Element of V; ::_thesis: for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
let F, G be FinSequence of V; ::_thesis: ( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v )
assume that
A1: len F = (len G) + 1 and
A2: G = F | (dom G) and
A3: v = F . (len F) ; ::_thesis: Sum F = (Sum G) + v
consider g being Function of NAT,V such that
A4: Sum G = g . (len G) and
A5: g . 0 = 0. V and
A6: for j being Element of NAT
for v being Element of V st j < len G & v = G . (j + 1) holds
g . (j + 1) = (g . j) + v by Def12;
consider f being Function of NAT,V such that
A7: Sum F = f . (len F) and
A8: f . 0 = 0. V and
A9: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by Def12;
defpred S1[ Element of NAT ] means  for H being FinSequence of V st len H = $1 & H = F | (Seg $1) & len H <= len G holds
f . (len H) = g . (len H);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_H_being_FinSequence_of_V_st_len_H_=_k_&_H_=_F_|_(Seg_k)_&_len_H_<=_len_G_holds_
f_._(len_H)_=_g_._(len_H)_)_holds_
for_H_being_FinSequence_of_V_st_len_H_=_k_+_1_&_H_=_F_|_(Seg_(k_+_1))_&_len_H_<=_len_G_holds_
f_._(len_H)_=_g_._(len_H)
let k be Element of NAT ; ::_thesis: ( ( for H being FinSequence of V st len H = k & H = F | (Seg k) & len H <= len G holds
f . (len H) = g . (len H) ) implies for H being FinSequence of V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H) )
assume A10: for H being FinSequence of V st len H = k & H = F | (Seg k) & len H <= len G holds
f . (len H) = g . (len H) ; ::_thesis: for H being FinSequence of V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H)
let H be FinSequence of V; ::_thesis: ( len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G implies f . (len H) = g . (len H) )
assume that
A11: len H = k + 1 and
A12: H = F | (Seg (k + 1)) and
A13: len H <= len G ; ::_thesis: f . (len H) = g . (len H)
 ( 1 <= k + 1 & k + 1 <= len F ) by A1, A11, A13, NAT_1:12;
then  k + 1 in dom F by FINSEQ_3:25;
then reconsider v = F . (k + 1) as Element of V by FUNCT_1:102;
 1 <= k + 1 by NAT_1:12;
then  k + 1 in Seg (len G) by A11, A13, FINSEQ_1:1;
then  k + 1 in dom G by FINSEQ_1:def_3;
then A14: v = G . (k + 1) by A2, FUNCT_1:47;
reconsider H1 = H as FinSequence of V ;
reconsider p = H1 | (Seg k) as FinSequence of V by FINSEQ_1:18;
A15: k <= len H by A11, NAT_1:12;
then  Seg k c= Seg (k + 1) by A11, FINSEQ_1:5;
then A16: p = F | (Seg k) by A12, FUNCT_1:51;
 k < k + 1 by XREAL_1:29;
then  k < len G by A11, A13, XXREAL_0:2;
then A17: g . (k + 1) = (g . k) + v by A6, A14;
A18: len G < len F by A1, XREAL_1:29;
 k <= len G by A13, A15, XXREAL_0:2;
then  k < len F by A18, XXREAL_0:2;
then A19: f . (k + 1) = (f . k) + v by A9;
 len p = k by A15, FINSEQ_1:17;
hence  f . (len H) = g . (len H) by A10, A11, A13, A15, A16, A19, A17, XXREAL_0:2; ::_thesis: verum
end;
then A20: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A21: dom G = Seg (len G) by FINSEQ_1:def_3;
A22: S1[ 0 ] by A8, A5;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A22, A20);
then  f . (len G) = g . (len G) by A2, A21;
hence  Sum F = (Sum G) + v by A1, A3, A7, A9, A4, XREAL_1:29; ::_thesis: verum
end;


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 & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
let V be RealLinearSpace; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = a * v ) implies Sum F = a * (Sum G) )
defpred S1[ set ] means  for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I);
A1: dom F = Seg (len F) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_a_*_v_)_holds_
Sum_H_=_a_*_(Sum_I)_)_holds_
for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_+_1_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_a_*_v_)_holds_
Sum_H_=_a_*_(Sum_I)
let n be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I) ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I) )
assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I) ; ::_thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) holds
Sum H = a * (Sum I)
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) implies Sum H = a * (Sum I) )
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ; ::_thesis: Sum H = a * (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then A7: len q = n by A3, A4, FINSEQ_1:17;
A8: len p = n by A4, A6, FINSEQ_1:17;
A9: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_p)_&_v_=_q_._k_holds_
p_._k_=_a_*_v
 len p <= len H by A4, A6, FINSEQ_1:17;
then A10: Seg (len p) c= Seg (len H) by FINSEQ_1:5;
A11: dom p = Seg n by A4, A6, FINSEQ_1:17;
let k be Element of NAT ; ::_thesis: for v being VECTOR of V st k in Seg (len p) & v = q . k holds
p . k = a * v
let v be VECTOR of V; ::_thesis: ( k in Seg (len p) & v = q . k implies p . k = a * v )
assume that
A12: k in Seg (len p) and
A13: v = q . k ; ::_thesis: p . k = a * v
 dom q = Seg n by A3, A4, A6, FINSEQ_1:17;
then  I . k = q . k by A8, A12, FUNCT_1:47;
then  H . k = a * v by A5, A12, A13, A10;
hence  p . k = a * v by A8, A12, A11, FUNCT_1:47; ::_thesis: verum
end;
 1 <= n + 1 by NAT_1:11;
then  ( n + 1 in dom H & n + 1 in dom I ) by A3, A4, FINSEQ_3:25;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as VECTOR of V by FUNCT_1:102;
A14: v1 = a * v2 by A4, A5, FINSEQ_1:4;
A15: dom q = Seg (len q) by FINSEQ_1:def_3;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  Sum H = (Sum p) + v1 by A4, A8, Th38
.= (a * (Sum q)) + (a * v2) by A2, A8, A7, A9, A14
.= a * ((Sum q) + v2) by Def5
.= a * (Sum I) by A3, A4, A7, A15, Th38 ;
::_thesis: verum
end;
then A16: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
now__::_thesis:_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_0_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_a_*_v_)_holds_
Sum_H_=_a_*_(Sum_I)
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ) implies Sum H = a * (Sum I) )
assume that
A17: len H = len I and
A18: len H = 0 and
 for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = a * v ; ::_thesis: Sum H = a * (Sum I)
 Sum H = 0. V by A18, Lm5;
hence  Sum H = a * (Sum I) by A17, A18, Lm5, Th10; ::_thesis: verum
end;
then A19: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A19, A16);
hence  ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = a * v ) implies Sum F = a * (Sum G) ) by A1; ::_thesis: verum
end;

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 & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) holds
Sum F = - (Sum G)
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) holds
Sum F = - (Sum G)
let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) )
defpred S1[ set ] means  for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I);
A1: dom F = Seg (len F) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_&_(_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_-_v_)_holds_
Sum_H_=_-_(Sum_I)_)_holds_
for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_n_+_1_&_(_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_-_v_)_holds_
Sum_H_=_-_(Sum_I)
let n be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) )
assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ; ::_thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) implies Sum H = - (Sum I) )
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ; ::_thesis: Sum H = - (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then A7: len q = n by A3, A4, FINSEQ_1:17;
A8: len p = n by A4, A6, FINSEQ_1:17;
A9: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_Seg_(len_p)_&_v_=_q_._k_holds_
p_._k_=_-_v
 len p <= len H by A4, A6, FINSEQ_1:17;
then A10: Seg (len p) c= Seg (len H) by FINSEQ_1:5;
A11: dom p = Seg n by A4, A6, FINSEQ_1:17;
let k be Element of NAT ; ::_thesis: for v being Element of V st k in Seg (len p) & v = q . k holds
p . k = - v
let v be Element of V; ::_thesis: ( k in Seg (len p) & v = q . k implies p . k = - v )
assume that
A12: k in Seg (len p) and
A13: v = q . k ; ::_thesis: p . k = - v
 dom q = Seg n by A3, A4, A6, FINSEQ_1:17;
then  I . k = q . k by A8, A12, FUNCT_1:47;
then  H . k = - v by A5, A12, A13, A10;
hence  p . k = - v by A8, A12, A11, FUNCT_1:47; ::_thesis: verum
end;
 1 <= n + 1 by NAT_1:11;
then  ( n + 1 in dom H & n + 1 in dom I ) by A3, A4, FINSEQ_3:25;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by FUNCT_1:102;
A14: v1 = - v2 by A4, A5, FINSEQ_1:4;
A15: dom q = Seg (len q) by FINSEQ_1:def_3;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  Sum H = (Sum p) + v1 by A4, A8, Th38
.= (- (Sum q)) + (- v2) by A2, A8, A7, A9, A14
.= - ((Sum q) + v2) by Lm3
.= - (Sum I) by A3, A4, A7, A15, Th38 ;
::_thesis: verum
end;
then A16: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
now__::_thesis:_for_H,_I_being_FinSequence_of_V_st_len_H_=_len_I_&_len_H_=_0_&_(_for_k_being_Element_of_NAT_
for_v_being_Element_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_-_v_)_holds_
Sum_H_=_-_(Sum_I)
let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) implies Sum H = - (Sum I) )
assume that
A17: ( len H = len I & len H = 0 ) and
 for k being Element of NAT
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ; ::_thesis: Sum H = - (Sum I)
 ( Sum H = 0. V & Sum I = 0. V ) by A17, Lm5;
hence  Sum H = - (Sum I) by Th12; ::_thesis: verum
end;
then A18: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A16);
hence  ( len F = len G & ( for k being Element of NAT
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) ) by A1; ::_thesis: verum
end;

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)
proof
let V be non empty add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of V holds Sum (F ^ G) = (Sum F) + (Sum G)
let F, G be FinSequence of V; ::_thesis: Sum (F ^ G) = (Sum F) + (Sum G)
defpred S1[ set ] means  for G being FinSequence of V st len G = $1 holds
Sum (F ^ G) = (Sum F) + (Sum G);
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for G being FinSequence of V st len G = k holds
Sum (F ^ G) = (Sum F) + (Sum G) ; ::_thesis: S1[k + 1]
let H be FinSequence of V; ::_thesis: ( len H = k + 1 implies Sum (F ^ H) = (Sum F) + (Sum H) )
reconsider p = H | (Seg k) as FinSequence of V by FINSEQ_1:18;
A3: rng H c= the carrier of V by FINSEQ_1:def_4;
assume A4: len H = k + 1 ; ::_thesis: Sum (F ^ H) = (Sum F) + (Sum H)
then A5: dom H = Seg (k + 1) by FINSEQ_1:def_3;
then A6: k + 1 in dom H by FINSEQ_1:4;
then  H . (k + 1) in rng H by FUNCT_1:def_3;
then reconsider v = H . (k + 1) as Element of V by A3;
A7: k <= k + 1 by NAT_1:12;
A8: now__::_thesis:_for_n_being_Nat_st_n_in_dom_p_holds_
p_._n_=_H_._n
let n be Nat; ::_thesis: ( n in dom p implies p . n = H . n )
assume  n in dom p ; ::_thesis: p . n = H . n
then  n in Seg k by A4, A7, FINSEQ_1:17;
hence  p . n = H . n by FUNCT_1:49; ::_thesis: verum
end;
A9: dom p = Seg (len p) by FINSEQ_1:def_3;
A10: Seg (len (F ^ p)) = Seg ((len F) + (len p)) by FINSEQ_1:22;
A11: dom (F ^ H) = Seg (len (F ^ H)) by FINSEQ_1:def_3
.= Seg ((len F) + (len H)) by FINSEQ_1:22 ;
A12: dom (F ^ p) = Seg (len (F ^ p)) by FINSEQ_1:def_3;
 dom p = Seg k by A4, A7, FINSEQ_1:17;
then A13: dom p c= dom H by A5, A7, FINSEQ_1:5;
A14: now__::_thesis:_for_x_being_set_st_x_in_dom_(F_^_p)_holds_
(F_^_p)_._x_=_(F_^_H)_._x
let x be set ; ::_thesis: ( x in dom (F ^ p) implies (F ^ p) . x = (F ^ H) . x )
assume A15: x in dom (F ^ p) ; ::_thesis: (F ^ p) . x = (F ^ H) . x
then reconsider n = x as Element of NAT ;
A16: now__::_thesis:_(_not_n_in_dom_F_implies_(F_^_p)_._x_=_(F_^_H)_._x_)
assume  not n in dom F ; ::_thesis: (F ^ p) . x = (F ^ H) . x
then A17: not n in Seg (len F) by FINSEQ_1:def_3;
A18: 1 <= n by A12, A15, FINSEQ_1:1;
then  len F <= n by A17, FINSEQ_1:1;
then consider j being Nat such that
A19: n = (len F) + j by NAT_1:10;
A20: now__::_thesis:_j_<=_k
assume  not j <= k ; ::_thesis: contradiction
then A21: (len F) + k < n by A19, XREAL_1:6;
 n <= (len F) + (len p) by A12, A10, A15, FINSEQ_1:1;
hence  contradiction by A4, A7, A21, FINSEQ_1:17; ::_thesis: verum
end;
now__::_thesis:_1_<=_j
assume  not 1 <= j ; ::_thesis: contradiction
then  j = 0 by NAT_1:14;
hence  contradiction by A17, A18, A19, FINSEQ_1:1; ::_thesis: verum
end;
then  j in Seg k by A20, FINSEQ_1:1;
then A22: j in dom p by A4, A7, FINSEQ_1:17;
then  ( (F ^ p) . n = p . j & (F ^ H) . n = H . j ) by A13, A19, FINSEQ_1:def_7;
hence  (F ^ p) . x = (F ^ H) . x by A8, A22; ::_thesis: verum
end;
now__::_thesis:_(_n_in_dom_F_implies_(F_^_p)_._x_=_(F_^_H)_._x_)
assume A23: n in dom F ; ::_thesis: (F ^ p) . x = (F ^ H) . x
then  (F ^ p) . n = F . n by FINSEQ_1:def_7;
hence  (F ^ p) . x = (F ^ H) . x by A23, FINSEQ_1:def_7; ::_thesis: verum
end;
hence  (F ^ p) . x = (F ^ H) . x by A16; ::_thesis: verum
end;
A24: len p = k by A4, A7, FINSEQ_1:17;
then  (len F) + (len p) <= (len F) + (len H) by A4, A7, XREAL_1:7;
then  Seg (len (F ^ p)) c= dom (F ^ H) by A11, A10, FINSEQ_1:5;
then  dom (F ^ p) = (dom (F ^ H)) /\ (Seg (len (F ^ p))) by A12, XBOOLE_1:28;
then A25: F ^ p = (F ^ H) | (Seg (len (F ^ p))) by A14, FUNCT_1:46
.= (F ^ H) | (dom (F ^ p)) by FINSEQ_1:def_3 ;
A26: now__::_thesis:_for_n_being_Nat_st_n_in_dom_<*v*>_holds_
H_._((len_p)_+_n)_=_<*v*>_._n
let n be Nat; ::_thesis: ( n in dom <*v*> implies H . ((len p) + n) = <*v*> . n )
assume  n in dom <*v*> ; ::_thesis: H . ((len p) + n) = <*v*> . n
then  n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then  n = 1 by TARSKI:def_1;
hence  H . ((len p) + n) = <*v*> . n by A24, FINSEQ_1:def_8; ::_thesis: verum
end;
 dom H = Seg ((len p) + (len <*v*>)) by A5, A24, FINSEQ_1:39;
then  H = p ^ <*v*> by A8, A26, FINSEQ_1:def_7;
then  F ^ H = (F ^ p) ^ <*v*> by FINSEQ_1:32;
then  len (F ^ H) = (len (F ^ p)) + (len <*v*>) by FINSEQ_1:22;
then A27: len (F ^ H) = (len (F ^ p)) + 1 by FINSEQ_1:39;
v = (F ^ H) . ((len F) + (len H)) by A4, A6, FINSEQ_1:def_7
.= (F ^ H) . (len (F ^ H)) by FINSEQ_1:22 ;
hence  Sum (F ^ H) = (Sum (F ^ p)) + v by A27, A25, Th38
.= ((Sum F) + (Sum p)) + v by A2, A24
.= (Sum F) + ((Sum p) + v) by Def3
.= (Sum F) + (Sum H) by A4, A24, A9, Th38 ;
::_thesis: verum
end;
A28: S1[ 0 ]
proof
let G be FinSequence of V; ::_thesis: ( len G = 0 implies Sum (F ^ G) = (Sum F) + (Sum G) )
assume  len G = 0 ; ::_thesis: Sum (F ^ G) = (Sum F) + (Sum G)
then  G = <*> the carrier of V ;
then  ( F ^ G = F & Sum G = 0. V ) by Lm4, FINSEQ_1:34;
hence  Sum (F ^ G) = (Sum F) + (Sum G) by Def4; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A28, A1);
then  ( len G = len G implies Sum (F ^ G) = (Sum F) + (Sum G) ) ;
hence  Sum (F ^ G) = (Sum F) + (Sum G) ; ::_thesis: verum
end;

         Lm6:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds Sum <*v*> = v
let v be Element of V; ::_thesis: Sum <*v*> = v
set S = <*v*>;
consider f being Function of NAT, the carrier of V such that
A1: Sum <*v*> = f . (len <*v*>) and
A2: ( f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len <*v*> & v = <*v*> . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by Def12;
 0 < 1 ;
then consider j being Element of NAT  such that
A3: j < len <*v*> ;
A4: len <*v*> = 1 by FINSEQ_1:39;
then A5: <*v*> . (j + 1) = <*v*> . (0 + 1) by A3, NAT_1:14
.= v by FINSEQ_1:40 ;
 j = 0 by A4, A3, NAT_1:14;
then f . 1 = (0. V) + v by A2, A5
.= v by Th4 ;
hence  Sum <*v*> = v by A1, FINSEQ_1:39; ::_thesis: verum
end;

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 & F is one-to-one & G is one-to-one holds
Sum F = Sum G
proof
let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of V st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G
let F, G be FinSequence of V; ::_thesis: ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G )
defpred S1[ set ] means  for H, I being FinSequence of V st len H = $1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I;
A1: len F = len F ;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_V_st_len_H_=_k_&_rng_H_=_rng_I_&_H_is_one-to-one_&_I_is_one-to-one_holds_
Sum_H_=_Sum_I_)_holds_
for_H,_I_being_FinSequence_of_V_st_len_H_=_k_+_1_&_rng_H_=_rng_I_&_H_is_one-to-one_&_I_is_one-to-one_holds_
Sum_H_=_Sum_I
let k be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ) implies for H, I being FinSequence of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I )
assume A2: for H, I being FinSequence of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ; ::_thesis: for H, I being FinSequence of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I
let H, I be FinSequence of V; ::_thesis: ( len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one implies Sum H = Sum I )
assume that
A3: len H = k + 1 and
A4: rng H = rng I and
A5: H is one-to-one and
A6: I is one-to-one ; ::_thesis: Sum H = Sum I
 k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A7: k + 1 in dom H by A3, FINSEQ_1:def_3;
then  H . (k + 1) in rng I by A4, FUNCT_1:def_3;
then consider x being set  such that
A8: x in dom I and
A9: H . (k + 1) = I . x by FUNCT_1:def_3;
reconsider v = H . (k + 1) as Element of V by A7, FUNCT_1:102;
reconsider n = x as Element of NAT by A8;
A10: len H = len I by A4, A5, A6, FINSEQ_1:48;
then A11: x in Seg (k + 1) by A3, A8, FINSEQ_1:def_3;
then A12: n <= k + 1 by FINSEQ_1:1;
then consider m2 being Nat such that
A13: n + m2 = k + 1 by NAT_1:10;
defpred S2[ Nat, set ] means $2 = I . (n + $1);
reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12;
A14: for j being Nat st j in Seg m2 holds
ex x being set st S2[j,x] ;
consider q2 being FinSequence such that
A15: dom q2 = Seg m2 and
A16: for k being Nat st k in Seg m2 holds
S2[k,q2 . k] from FINSEQ_1:sch_1(A14);
A17: rng q2 c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q2 or x in the carrier of V )
assume  x in rng q2 ; ::_thesis: x in the carrier of V
then consider y being set  such that
A18: y in dom q2 and
A19: x = q2 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A18;
 1 <= y by A15, A18, FINSEQ_1:1;
then A20: 1 <= n + y by NAT_1:12;
 y <= m2 by A15, A18, FINSEQ_1:1;
then  n + y <= len I by A3, A10, A13, XREAL_1:7;
then  n + y in dom I by A20, FINSEQ_3:25;
then reconsider xx = I . (n + y) as Element of V by FUNCT_1:102;
 xx in the carrier of V ;
hence  x in the carrier of V by A15, A16, A18, A19; ::_thesis: verum
end;
reconsider p = H | (Seg k) as FinSequence of V by FINSEQ_1:18;
A21: p is one-to-one by A5, FUNCT_1:52;
 Seg k = (Seg (k + 1)) \ {(k + 1)} by FINSEQ_1:10;
then A22: H .: (Seg k) = (H .: (Seg (k + 1))) \ (Im (H,(k + 1))) by A5, FUNCT_1:64;
A23: 1 <= n by A11, FINSEQ_1:1;
then consider m1 being Nat such that
A24: 1 + m1 = n by NAT_1:10;
reconsider q1 = I | (Seg m1) as FinSequence of V by FINSEQ_1:18;
reconsider q2 = q2 as FinSequence of V by A17, FINSEQ_1:def_4;
 m1 <= n by A24, NAT_1:11;
then A25: m1 <= k + 1 by A12, XXREAL_0:2;
then A26: len q1 = m1 by A3, A10, FINSEQ_1:17;
A27: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_
I_._((len_(q1_^_<*v*>))_+_j)_=_q2_._j
let j be Nat; ::_thesis: ( j in dom q2 implies I . ((len (q1 ^ <*v*>)) + j) = q2 . j )
assume A28: j in dom q2 ; ::_thesis: I . ((len (q1 ^ <*v*>)) + j) = q2 . j
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A26, FINSEQ_1:22
.= n by A24, FINSEQ_1:39 ;
hence  I . ((len (q1 ^ <*v*>)) + j) = q2 . j by A15, A16, A28; ::_thesis: verum
end;
set q = q1 ^ q2;
A29: m1 < n by A24, XREAL_1:29;
A30: {v} misses rng (q1 ^ q2)
proof
set y = the Element of {v} /\ (rng (q1 ^ q2));
assume  not {v} misses rng (q1 ^ q2) ; ::_thesis: contradiction
then A31: {v} /\ (rng (q1 ^ q2)) <> {} by XBOOLE_0:def_7;
then A32: the Element of {v} /\ (rng (q1 ^ q2)) in {v} by XBOOLE_0:def_4;
A33: now__::_thesis:_not_the_Element_of_{v}_/\_(rng_(q1_^_q2))_in_rng_q1
assume  the Element of {v} /\ (rng (q1 ^ q2)) in rng q1 ; ::_thesis: contradiction
then consider y1 being set  such that
A34: y1 in dom q1 and
A35: the Element of {v} /\ (rng (q1 ^ q2)) = q1 . y1 by FUNCT_1:def_3;
A36: y1 in Seg m1 by A3, A10, A25, A34, FINSEQ_1:17;
reconsider y1 = y1 as Element of NAT by A34;
 y1 <= m1 by A36, FINSEQ_1:1;
then A37: y1 <= k + 1 by A25, XXREAL_0:2;
 1 <= y1 by A36, FINSEQ_1:1;
then  y1 in Seg (k + 1) by A37, FINSEQ_1:1;
then A38: y1 in dom I by A3, A10, FINSEQ_1:def_3;
 q1 . y1 = I . y1 by A34, FUNCT_1:47;
then A39: I . y1 = I . n by A9, A32, A35, TARSKI:def_1;
 y1 <> n by A29, A36, FINSEQ_1:1;
hence  contradiction by A6, A8, A38, A39, FUNCT_1:def_4; ::_thesis: verum
end;
A40: the Element of {v} /\ (rng (q1 ^ q2)) = I . n by A9, A32, TARSKI:def_1;
A41: now__::_thesis:_not_the_Element_of_{v}_/\_(rng_(q1_^_q2))_in_rng_q2
assume  the Element of {v} /\ (rng (q1 ^ q2)) in rng q2 ; ::_thesis: contradiction
then consider y1 being set  such that
A42: y1 in dom q2 and
A43: the Element of {v} /\ (rng (q1 ^ q2)) = q2 . y1 by FUNCT_1:def_3;
reconsider y1 = y1 as Element of NAT by A42;
 y1 <= m2 by A15, A42, FINSEQ_1:1;
then A44: n + y1 <= k + 1 by A13, XREAL_1:7;
 1 <= n + y1 by A23, NAT_1:12;
then  n + y1 in Seg (k + 1) by A44, FINSEQ_1:1;
then A45: n + y1 in dom I by A3, A10, FINSEQ_1:def_3;
 I . n = I . (n + y1) by A15, A16, A40, A42, A43;
then A46: n = n + y1 by A6, A8, A45, FUNCT_1:def_4;
 y1 <> 0 by A15, A42, FINSEQ_1:1;
hence  contradiction by A46; ::_thesis: verum
end;
 the Element of {v} /\ (rng (q1 ^ q2)) in rng (q1 ^ q2) by A31, XBOOLE_0:def_4;
then  the Element of {v} /\ (rng (q1 ^ q2)) in (rng q1) \/ (rng q2) by FINSEQ_1:31;
hence  contradiction by A33, A41, XBOOLE_0:def_3; ::_thesis: verum
end;
A47: q1 ^ q2 is one-to-one
proof
let y1, y2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not y1 in dom (q1 ^ q2) or not y2 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that
A48: ( y1 in dom (q1 ^ q2) & y2 in dom (q1 ^ q2) ) and
A49: (q1 ^ q2) . y1 = (q1 ^ q2) . y2 ; ::_thesis: y1 = y2
reconsider x1 = y1, x2 = y2 as Element of NAT by A48;
A50: now__::_thesis:_(_ex_j1_being_Nat_st_
(_j1_in_dom_q2_&_x1_=_(len_q1)_+_j1_)_&_ex_j2_being_Nat_st_
(_j2_in_dom_q2_&_x2_=_(len_q1)_+_j2_)_implies_y1_=_y2_)
given j1 being Nat such that A51: j1 in dom q2 and
A52: x1 = (len q1) + j1 ; ::_thesis: ( ex j2 being Nat st
( j2 in dom q2 & x2 = (len q1) + j2 ) implies y1 = y2 )
A53: q2 . j1 = I . (n + j1) by A15, A16, A51;
 j1 <= m2 by A15, A51, FINSEQ_1:1;
then A54: n + j1 <= k + 1 by A13, XREAL_1:7;
 1 <= n + j1 by A23, NAT_1:12;
then  n + j1 in Seg (k + 1) by A54, FINSEQ_1:1;
then A55: n + j1 in dom I by A3, A10, FINSEQ_1:def_3;
given j2 being Nat such that A56: j2 in dom q2 and
A57: x2 = (len q1) + j2 ; ::_thesis: y1 = y2
A58: q2 . j2 = I . (n + j2) by A15, A16, A56;
 j2 <= m2 by A15, A56, FINSEQ_1:1;
then A59: n + j2 <= k + 1 by A13, XREAL_1:7;
 1 <= n + j2 by A23, NAT_1:12;
then  n + j2 in Seg (k + 1) by A59, FINSEQ_1:1;
then A60: n + j2 in dom I by A3, A10, FINSEQ_1:def_3;
q2 . j1 = (q1 ^ q2) . (m1 + j2) by A26, A49, A51, A52, A57, FINSEQ_1:def_7
.= q2 . j2 by A26, A56, FINSEQ_1:def_7 ;
then  n + j1 = n + j2 by A6, A53, A58, A55, A60, FUNCT_1:def_4;
hence  y1 = y2 by A52, A57; ::_thesis: verum
end;
A61: now__::_thesis:_(_x2_in_dom_q1_&_ex_j_being_Nat_st_
(_j_in_dom_q2_&_x1_=_(len_q1)_+_j_)_implies_y1_=_y2_)
assume A62: x2 in dom q1 ; ::_thesis: ( ex j being Nat st
( j in dom q2 & x1 = (len q1) + j ) implies y1 = y2 )
then  q1 . x2 = I . x2 by FUNCT_1:47;
then A63: (q1 ^ q2) . x2 = I . x2 by A62, FINSEQ_1:def_7;
A64: x2 in Seg m1 by A3, A10, A25, A62, FINSEQ_1:17;
then A65: 1 <= x2 by FINSEQ_1:1;
A66: x2 <= m1 by A64, FINSEQ_1:1;
then  x2 <= k + 1 by A25, XXREAL_0:2;
then  x2 in Seg (k + 1) by A65, FINSEQ_1:1;
then A67: x2 in dom I by A3, A10, FINSEQ_1:def_3;
given j being Nat such that A68: j in dom q2 and
A69: x1 = (len q1) + j ; ::_thesis: y1 = y2
 q2 . j = I . (n + j) by A15, A16, A68;
then A70: I . x2 = I . (n + j) by A49, A68, A69, A63, FINSEQ_1:def_7;
 j <= m2 by A15, A68, FINSEQ_1:1;
then A71: n + j <= k + 1 by A13, XREAL_1:7;
 1 <= n + j by A23, NAT_1:12;
then  n + j in Seg (k + 1) by A71, FINSEQ_1:1;
then A72: n + j in dom I by A3, A10, FINSEQ_1:def_3;
A73: n <= n + j by NAT_1:12;
 x2 < n by A29, A66, XXREAL_0:2;
hence  y1 = y2 by A6, A70, A67, A72, A73, FUNCT_1:def_4; ::_thesis: verum
end;
A74: now__::_thesis:_(_x1_in_dom_q1_&_ex_j_being_Nat_st_
(_j_in_dom_q2_&_x2_=_(len_q1)_+_j_)_implies_y1_=_y2_)
assume A75: x1 in dom q1 ; ::_thesis: ( ex j being Nat st
( j in dom q2 & x2 = (len q1) + j ) implies y1 = y2 )
then  q1 . x1 = I . x1 by FUNCT_1:47;
then A76: (q1 ^ q2) . x1 = I . x1 by A75, FINSEQ_1:def_7;
A77: x1 in Seg m1 by A3, A10, A25, A75, FINSEQ_1:17;
then A78: 1 <= x1 by FINSEQ_1:1;
A79: x1 <= m1 by A77, FINSEQ_1:1;
then  x1 <= k + 1 by A25, XXREAL_0:2;
then  x1 in Seg (k + 1) by A78, FINSEQ_1:1;
then A80: x1 in dom I by A3, A10, FINSEQ_1:def_3;
given j being Nat such that A81: j in dom q2 and
A82: x2 = (len q1) + j ; ::_thesis: y1 = y2
 q2 . j = I . (n + j) by A15, A16, A81;
then A83: I . x1 = I . (n + j) by A49, A81, A82, A76, FINSEQ_1:def_7;
 j <= m2 by A15, A81, FINSEQ_1:1;
then A84: n + j <= k + 1 by A13, XREAL_1:7;
 1 <= n + j by A23, NAT_1:12;
then  n + j in Seg (k + 1) by A84, FINSEQ_1:1;
then A85: n + j in dom I by A3, A10, FINSEQ_1:def_3;
A86: n <= n + j by NAT_1:12;
 x1 < n by A29, A79, XXREAL_0:2;
hence  y1 = y2 by A6, A83, A80, A85, A86, FUNCT_1:def_4; ::_thesis: verum
end;
A87: q1 is one-to-one by A6, FUNCT_1:52;
now__::_thesis:_(_x1_in_dom_q1_&_x2_in_dom_q1_implies_y1_=_y2_)
assume A88: ( x1 in dom q1 & x2 in dom q1 ) ; ::_thesis: y1 = y2
then  ( q1 . x1 = (q1 ^ q2) . x1 & q1 . x2 = (q1 ^ q2) . x2 ) by FINSEQ_1:def_7;
hence  y1 = y2 by A49, A87, A88, FUNCT_1:def_4; ::_thesis: verum
end;
hence  y1 = y2 by A48, A74, A61, A50, FINSEQ_1:25; ::_thesis: verum
end;
 k <= k + 1 by NAT_1:12;
then A89: len p = k by A3, FINSEQ_1:17;
A90: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<*v*>_holds_
H_._((len_p)_+_k)_=_<*v*>_._k
let k be Nat; ::_thesis: ( k in dom <*v*> implies H . ((len p) + k) = <*v*> . k )
assume  k in dom <*v*> ; ::_thesis: H . ((len p) + k) = <*v*> . k
then  k in Seg 1 by FINSEQ_1:38;
then  k = 1 by FINSEQ_1:2, TARSKI:def_1;
hence  H . ((len p) + k) = <*v*> . k by A89, FINSEQ_1:40; ::_thesis: verum
end;
A91: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*v*>)_holds_
I_._j_=_(q1_^_<*v*>)_._j
let j be Nat; ::_thesis: ( j in dom (q1 ^ <*v*>) implies I . j = (q1 ^ <*v*>) . j )
assume A92: j in dom (q1 ^ <*v*>) ; ::_thesis: I . j = (q1 ^ <*v*>) . j
A93: now__::_thesis:_(_j_in_Seg_m1_implies_I_._j_=_(q1_^_<*v*>)_._j_)
assume  j in Seg m1 ; ::_thesis: I . j = (q1 ^ <*v*>) . j
then A94: j in dom q1 by A3, A10, A25, FINSEQ_1:17;
then  q1 . j = I . j by FUNCT_1:47;
hence  I . j = (q1 ^ <*v*>) . j by A94, FINSEQ_1:def_7; ::_thesis: verum
end;
A95: now__::_thesis:_(_j_in_{n}_implies_(q1_^_<*v*>)_._j_=_I_._j_)
 ( 1 in Seg 1 & len <*v*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39;
then  1 in dom <*v*> by FINSEQ_1:def_3;
then A96: (q1 ^ <*v*>) . ((len q1) + 1) = <*v*> . 1 by FINSEQ_1:def_7;
assume  j in {n} ; ::_thesis: (q1 ^ <*v*>) . j = I . j
then  j = n by TARSKI:def_1;
hence  (q1 ^ <*v*>) . j = I . j by A9, A24, A26, A96, FINSEQ_1:40; ::_thesis: verum
end;
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A26, FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40 ;
then  j in Seg (m1 + 1) by A92, FINSEQ_1:def_3;
then  j in (Seg m1) \/ {n} by A24, FINSEQ_1:9;
hence  I . j = (q1 ^ <*v*>) . j by A93, A95, XBOOLE_0:def_3; ::_thesis: verum
end;
 len q2 = m2 by A15, FINSEQ_1:def_3;
then (len (q1 ^ <*v*>)) + (len q2) = ((len q1) + (len <*v*>)) + m2 by FINSEQ_1:22
.= k + 1 by A24, A13, A26, FINSEQ_1:40 ;
then  dom I = Seg ((len (q1 ^ <*v*>)) + (len q2)) by A3, A10, FINSEQ_1:def_3;
then A97: I = (q1 ^ <*v*>) ^ q2 by A91, A27, FINSEQ_1:def_7;
then  rng I = (rng (q1 ^ <*v*>)) \/ (rng q2) by FINSEQ_1:31
.= ((rng <*v*>) \/ (rng q1)) \/ (rng q2) by FINSEQ_1:31
.= ({v} \/ (rng q1)) \/ (rng q2) by FINSEQ_1:39
.= {v} \/ ((rng q1) \/ (rng q2)) by XBOOLE_1:4
.= {v} \/ (rng (q1 ^ q2)) by FINSEQ_1:31 ;
then A98: rng (q1 ^ q2) = (rng I) \ {v} by A30, XBOOLE_1:88;
A99: Seg (k + 1) = dom H by A3, FINSEQ_1:def_3;
then  ( rng p = H .: (Seg k) & rng H = H .: (Seg (k + 1)) ) by RELAT_1:113, RELAT_1:115;
then A100: rng p = rng (q1 ^ q2) by A4, A98, A99, A22, FINSEQ_1:4, FUNCT_1:59;
 ( len <*v*> = 1 & ( for k being Nat st k in dom p holds
H . k = p . k ) ) by FINSEQ_1:39, FUNCT_1:47;
then  H = p ^ <*v*> by A89, A99, A90, FINSEQ_1:def_7;
then A101: Sum H = (Sum p) + (Sum <*v*>) by Th41;
Sum I = (Sum (q1 ^ <*v*>)) + (Sum q2) by A97, Th41
.= ((Sum q1) + (Sum <*v*>)) + (Sum q2) by Th41
.= (Sum <*v*>) + ((Sum q1) + (Sum q2)) by Def3
.= (Sum (q1 ^ q2)) + (Sum <*v*>) by Th41 ;
hence  Sum H = Sum I by A2, A89, A100, A21, A47, A101; ::_thesis: verum
end;
then A102: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
now__::_thesis:_for_H,_I_being_FinSequence_of_V_st_len_H_=_0_&_rng_H_=_rng_I_&_H_is_one-to-one_&_I_is_one-to-one_holds_
Sum_H_=_Sum_I
let H, I be FinSequence of V; ::_thesis: ( len H = 0 & rng H = rng I & H is one-to-one & I is one-to-one implies Sum H = Sum I )
assume that
A103: len H = 0 and
A104: rng H = rng I and
 H is one-to-one and
 I is one-to-one ; ::_thesis: Sum H = Sum I
 H = {} by A103;
then  I = {} by A104;
then A105: len I = 0 ;
 Sum H = 0. V by A103, Lm5;
hence  Sum H = Sum I by A105, Lm5; ::_thesis: verum
end;
then A106: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A106, A102);
hence  ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G ) by A1; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V holds Sum <*v,u*> = v + u
let v, u be Element of V; ::_thesis: Sum <*v,u*> = v + u
 <*v,u*> = <*v*> ^ <*u*> by FINSEQ_1:def_9;
hence  Sum <*v,u*> = (Sum <*v*>) + (Sum <*u*>) by Th41
.= v + (Sum <*u*>) by Lm6
.= v + u by Lm6 ;
::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*v,u,w*> = (v + u) + w
let v, u, w be Element of V; ::_thesis: Sum <*v,u,w*> = (v + u) + w
 <*v,u,w*> = <*v,u*> ^ <*w*> by FINSEQ_1:43;
hence  Sum <*v,u,w*> = (Sum <*v,u*>) + (Sum <*w*>) by Th41
.= (Sum <*v,u*>) + w by Lm6
.= (v + u) + w by Th45 ;
::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let a be Real; ::_thesis: for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let v, u be VECTOR of V; ::_thesis: a * (Sum <*v,u*>) = (a * v) + (a * u)
thus a * (Sum <*v,u*>) = a * (v + u) by Th45
.= (a * v) + (a * u) by Def5 ; ::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: for a being Real
for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let a be Real; ::_thesis: for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let v, u, w be VECTOR of V; ::_thesis: a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
thus a * (Sum <*v,u,w*>) = a * ((v + u) + w) by Th46
.= (a * (v + u)) + (a * w) by Def5
.= ((a * v) + (a * u)) + (a * w) by Def5 ; ::_thesis: verum
end;

theorem :: RLVECT_1:50
for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: - (Sum (<*> the carrier of V)) = 0. V
thus  - (Sum (<*> the carrier of V)) = - (0. V) by Lm4
.= 0. V by Th12 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u
let v, u be Element of V; ::_thesis: - (Sum <*v,u*>) = (- v) - u
thus  - (Sum <*v,u*>) = - (v + u) by Th45
.= (- v) - u by Th30 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w
let v, u, w be Element of V; ::_thesis: - (Sum <*v,u,w*>) = ((- v) - u) - w
thus  - (Sum <*v,u,w*>) = - ((v + u) + w) by Th46
.= (- (v + u)) - w by Th30
.= ((- v) - u) - w by Th30 ; ::_thesis: verum
end;

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*>
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds Sum <*v,w*> = Sum <*w,v*>
let v, w be Element of V; ::_thesis: Sum <*v,w*> = Sum <*w,v*>
thus  Sum <*v,w*> = v + w by Th45
.= Sum <*w,v*> by Th45 ; ::_thesis: verum
end;

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*>)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)
let v, w be Element of V; ::_thesis: Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)
thus  Sum <*v,w*> = v + w by Th45
.= (Sum <*v*>) + w by Lm6
.= (Sum <*v*>) + (Sum <*w*>) by Lm6 ; ::_thesis: verum
end;

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 & Sum <*v,(0. V)*> = v )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )
let v be Element of V; ::_thesis: ( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )
thus  Sum <*(0. V),v*> = (0. V) + v by Th45
.= v by Th4 ; ::_thesis: Sum <*v,(0. V)*> = v
thus  Sum <*v,(0. V)*> = v + (0. V) by Th45
.= v by Th4 ; ::_thesis: verum
end;

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 & Sum <*(- v),v*> = 0. V )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )
let v be Element of V; ::_thesis: ( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )
A1: v + (- v) = 0. V by Def10;
hence  Sum <*v,(- v)*> = 0. V by Th45; ::_thesis: Sum <*(- v),v*> = 0. V
 (- v) + v = 0. V by A1, Lm1;
hence  Sum <*(- v),v*> = 0. V by Th45; ::_thesis: verum
end;

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)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds Sum <*(- v),(- w)*> = - (w + v)
let v, w be Element of V; ::_thesis: Sum <*(- v),(- w)*> = - (w + v)
thus  Sum <*(- v),(- w)*> = (- v) + (- w) by Th45
.= - (w + v) by Lm3 ; ::_thesis: verum
end;

theorem Th61: :: RLVECT_1:61
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v*> = 2 * v
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*v,v*> = 2 * v
let v be VECTOR of V; ::_thesis: Sum <*v,v*> = 2 * v
thus  Sum <*v,v*> = v + v by Th45
.= (1 * v) + v by Def8
.= (1 * v) + (1 * v) by Def8
.= (1 + 1) * v by Def6
.= 2 * v ; ::_thesis: verum
end;

theorem :: RLVECT_1:62
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- 2) * v
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- 2) * v
let v be VECTOR of V; ::_thesis: Sum <*(- v),(- v)*> = (- 2) * v
thus  Sum <*(- v),(- v)*> = - (v + v) by Th60
.= - (Sum <*v,v*>) by Th45
.= - (2 * v) by Th61
.= (- 1) * (2 * v) by Th16
.= ((- 1) * 2) * v by Def7
.= (- 2) * v ; ::_thesis: verum
end;

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*>)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for u, v, w being Element of V holds Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)
let u, v, w be Element of V; ::_thesis: Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= ((Sum <*u*>) + v) + w by Lm6
.= ((Sum <*u*>) + v) + (Sum <*w*>) by Lm6
.= ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>) by Lm6 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for u, v, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,v*>) + w
let u, v, w be Element of V; ::_thesis: Sum <*u,v,w*> = (Sum <*u,v*>) + w
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= (Sum <*u,v*>) + w by Th45 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*v,w*>) + u
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = (Sum <*v,w*>) + u
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= u + (v + w) by Def3
.= (Sum <*v,w*>) + u by Th45 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = (Sum <*u,w*>) + v
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = (Sum <*u,w*>) + v
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= (u + w) + v by Def3
.= (Sum <*u,w*>) + v by Th45 ; ::_thesis: verum
end;

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*>
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*u,w,v*>
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = Sum <*u,w,v*>
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= (u + w) + v by Def3
.= Sum <*u,w,v*> by Th46 ; ::_thesis: verum
end;

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*>
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,u,w*>
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = Sum <*v,u,w*>
thus  Sum <*u,v,w*> = (u + v) + w by Th46
.= Sum <*v,u,w*> by Th46 ; ::_thesis: verum
end;

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*>
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*v,w,u*>
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = Sum <*v,w,u*>
thus  Sum <*u,v,w*> = Sum <*v,u,w*> by Th68
.= Sum <*v,w,u*> by Th67 ; ::_thesis: verum
end;

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*>
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds Sum <*u,v,w*> = Sum <*w,v,u*>
let v, u, w be Element of V; ::_thesis: Sum <*u,v,w*> = Sum <*w,v,u*>
thus  Sum <*u,v,w*> = Sum <*w,u,v*> by Th69
.= Sum <*w,v,u*> by Th67 ; ::_thesis: verum
end;

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 & Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( Sum <*(0. V),(0. V),v*> = v & Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )
let v be Element of V; ::_thesis: ( Sum <*(0. V),(0. V),v*> = v & Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )
thus  Sum <*(0. V),(0. V),v*> = ((0. V) + (0. V)) + v by Th46
.= (0. V) + v by Th4
.= v by Th4 ; ::_thesis: ( Sum <*(0. V),v,(0. V)*> = v & Sum <*v,(0. V),(0. V)*> = v )
thus  Sum <*(0. V),v,(0. V)*> = ((0. V) + v) + (0. V) by Th46
.= (0. V) + v by Th4
.= v by Th4 ; ::_thesis: Sum <*v,(0. V),(0. V)*> = v
thus  Sum <*v,(0. V),(0. V)*> = (v + (0. V)) + (0. V) by Th46
.= v + (0. V) by Th4
.= v by Th4 ; ::_thesis: verum
end;

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 & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for u, v being Element of V holds
( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
let u, v be Element of V; ::_thesis: ( Sum <*(0. V),u,v*> = u + v & Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
thus  Sum <*(0. V),u,v*> = ((0. V) + u) + v by Th46
.= u + v by Th4 ; ::_thesis: ( Sum <*u,v,(0. V)*> = u + v & Sum <*u,(0. V),v*> = u + v )
thus  Sum <*u,v,(0. V)*> = (u + v) + (0. V) by Th46
.= u + v by Th4 ; ::_thesis: Sum <*u,(0. V),v*> = u + v
thus  Sum <*u,(0. V),v*> = (u + (0. V)) + v by Th46
.= u + v by Th4 ; ::_thesis: verum
end;

theorem :: RLVECT_1:74
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v,v*> = 3 * v
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*v,v,v*> = 3 * v
let v be VECTOR of V; ::_thesis: Sum <*v,v,v*> = 3 * v
thus  Sum <*v,v,v*> = (Sum <*v,v*>) + v by Th66
.= (2 * v) + v by Th61
.= (2 * v) + (1 * v) by Def8
.= (2 + 1) * v by Def6
.= 3 * v ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of V st len F = 1 holds
Sum F = F . 1
let F be FinSequence of V; ::_thesis: ( len F = 1 implies Sum F = F . 1 )
assume A1: len F = 1 ; ::_thesis: Sum F = F . 1
then  dom F = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then  1 in dom F by TARSKI:def_1;
then A2: F . 1 in rng F by FUNCT_1:def_3;
 rng F c= the carrier of V by FINSEQ_1:def_4;
then reconsider v = F . 1 as Element of V by A2;
 F = <*v*> by A1, FINSEQ_1:40;
hence  Sum F = F . 1 by Lm6; ::_thesis: verum
end;

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 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of V
for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2
let F be FinSequence of V; ::_thesis: for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2
let v1, v2 be Element of V; ::_thesis: ( len F = 2 & v1 = F . 1 & v2 = F . 2 implies Sum F = v1 + v2 )
assume  ( len F = 2 & v1 = F . 1 & v2 = F . 2 ) ; ::_thesis: Sum F = v1 + v2
then  F = <*v1,v2*> by FINSEQ_1:44;
hence  Sum F = v1 + v2 by Th45; ::_thesis: verum
end;

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 & v1 = F . 1 & v2 = F . 2 & v = F . 3 holds
Sum F = (v1 + v2) + v
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of V
for v1, v2, v being Element of V st len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 holds
Sum F = (v1 + v2) + v
let F be FinSequence of V; ::_thesis: for v1, v2, v being Element of V st len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 holds
Sum F = (v1 + v2) + v
let v1, v2, v be Element of V; ::_thesis: ( len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 implies Sum F = (v1 + v2) + v )
assume  ( len F = 3 & v1 = F . 1 & v2 = F . 2 & v = F . 3 ) ; ::_thesis: Sum F = (v1 + v2) + v
then  F = <*v1,v2,v*> by FINSEQ_1:45;
hence  Sum F = (v1 + v2) + v by Th46; ::_thesis: verum
end;

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 & (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 & (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
proof
let L be non empty addLoopStr ; ::_thesis: ( L is zeroed implies L is right_zeroed )
assume  L is zeroed ; ::_thesis: L is right_zeroed
hence  for v being Element of L holds v + (0. L) = v by Def13; :: according to RLVECT_1:def_4 ::_thesis: verum
end;
end;

registration
cluster non empty Abelian right_zeroed  ->  non empty zeroed for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Abelian & b1 is right_zeroed holds
b1 is zeroed
proof
let L be non empty addLoopStr ; ::_thesis: ( L is Abelian & L is right_zeroed implies L is zeroed )
assume A1: ( L is Abelian & L is right_zeroed ) ; ::_thesis: L is zeroed
let a be Element of L; :: according to RLVECT_1:def_13 ::_thesis: ( a + (0. L) = a & (0. L) + a = a )
thus  a + (0. L) = a by A1, Def4; ::_thesis: (0. L) + a = a
hence  (0. L) + a = a by A1, Def2; ::_thesis: verum
end;
cluster non empty right_complementable Abelian  ->  non empty left_complementable for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Abelian & b1 is right_complementable holds
b1 is left_complementable
proof
let L be non empty addLoopStr ; ::_thesis: ( L is Abelian & L is right_complementable implies L is left_complementable )
assume A2: ( L is Abelian & L is right_complementable ) ; ::_thesis: L is left_complementable
let a be Element of L; :: according to ALGSTR_0:def_15 ::_thesis: a is left_complementable
consider w being Element of L such that
A3: a + w = 0. L by A2, ALGSTR_0:def_11;
take  w ; :: according to ALGSTR_0:def_10 ::_thesis: w + a = 0. L
thus  w + a = 0. L by A2, A3, Def2; ::_thesis: verum
end;
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)
proof
let a be real number ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds (- a) * v = - (a * v)
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds (- a) * v = - (a * v)
let v be VECTOR of V; ::_thesis: (- a) * v = - (a * v)
thus (- a) * v = a * (- v) by Th24
.= - (a * v) by Th25 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: - (Sum (<*> the carrier of V)) = 0. V
thus  - (Sum (<*> the carrier of V)) = - (0. V) by Th43
.= 0. V by Th12 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u
let v, u be Element of V; ::_thesis: - (Sum <*v,u*>) = (- v) - u
thus  - (Sum <*v,u*>) = - (v + u) by Th45
.= (- v) - u by Th30 ; ::_thesis: verum
end;

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
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w
let v, u, w be Element of V; ::_thesis: - (Sum <*v,u,w*>) = ((- v) - u) - w
thus  - (Sum <*v,u,w*>) = - ((v + u) + w) by Th46
.= (- (v + u)) - w by Th30
.= ((- v) - u) - w by Th30 ; ::_thesis: verum
end;

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 & Sum <*(- v),v*> = 0. V )
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds
( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )
let v be Element of V; ::_thesis: ( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )
thus  Sum <*v,(- v)*> = v + (- v) by Th45
.= 0. V by Th5 ; ::_thesis: Sum <*(- v),v*> = 0. V
hence  Sum <*(- v),v*> = 0. V by Th54; ::_thesis: verum
end;

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 & Sum <*(- w),v*> = v - w )
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds
( Sum <*v,(- w)*> = v - w & Sum <*(- w),v*> = v - w )
let v, w be Element of V; ::_thesis: ( Sum <*v,(- w)*> = v - w & Sum <*(- w),v*> = v - w )
thus  Sum <*v,(- w)*> = v + (- w) by Th45
.= v - w ; ::_thesis: Sum <*(- w),v*> = v - w
hence  Sum <*(- w),v*> = v - w by Th54; ::_thesis: verum
end;

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) & Sum <*(- w),(- v)*> = - (v + w) )
proof
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds
( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )
let v, w be Element of V; ::_thesis: ( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )
thus  Sum <*(- v),(- w)*> = (- v) + (- w) by Th45
.= - (v + w) by Th31 ; ::_thesis: Sum <*(- w),(- v)*> = - (v + w)
hence  Sum <*(- w),(- v)*> = - (v + w) by Th54; ::_thesis: verum
end;