:: RLVECT_1 semantic presentation

definition

attr a₁ is strict;
struct LoopStr -> ZeroStr ;
aggr LoopStr(# carrier, add, Zero #) -> LoopStr ;
sel add c₁ -> BinOp of the carrier of a₁;

end;

definition

attr a₁ is strict;
struct RLSStruct -> LoopStr ;
aggr RLSStruct(# carrier, Zero, add, Mult #) -> RLSStruct ;
sel Mult c₁ -> Function of [:REAL ,the carrier of a₁:],the carrier of a₁;

end;

registration

cluster non empty RLSStruct ;
existence

proof end;

end;

definition

let c₁ be RLSStruct ;
mode VECTOR of a₁ is Element of a₁;

end;

definition

let c₁ be 1-sorted ;
let c₂ be set ;
pred c₂ in c₁ means :Def1: :: RLVECT_1:def 1
a₂ in the carrier of a₁;

end;

:: deftheorem Def1 defines in RLVECT_1:def 1 :

theorem Th1: :: RLVECT_1:1

canceled;

theorem Th2: :: RLVECT_1:2

canceled;

theorem Th3: :: RLVECT_1:3

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ holds b₂ in b₁ by Def1;

definition

let c₁ be ZeroStr ;
func 0. c₁ -> Element of a₁ equals :: RLVECT_1:def 2
the Zero of a₁;
coherence ;

end;

:: deftheorem Def2 defines 0. RLVECT_1:def 2 :

registration

cluster non empty strict LoopStr ;
existence

proof end;

end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Element of c₁;
func c₂ + c₃ -> Element of a₁ equals :: RLVECT_1:def 3
the add of a₁ . [a₂,a₃];
coherence ;

end;

:: deftheorem Def3 defines + RLVECT_1:def 3 :

definition

let c₁ be non empty RLSStruct ;
let c₂ be VECTOR of c₁;
let c₃ be Real;
func c₃ * c₂ -> Element of a₁ equals :: RLVECT_1:def 4
the Mult of a₁ . [a₃,a₂];
coherence ;

end;

:: deftheorem Def4 defines * RLVECT_1:def 4 :

theorem Th4: :: RLVECT_1:4

canceled;

theorem Th5: :: RLVECT_1:5

for b₁ being non empty LoopStr
for b₂, b₃ being Element of b₁ holds b₂ + b₃ = the add of b₁ . b₂,b₃ ;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:REAL ,c₁:],c₁;
cluster RLSStruct(# a₁,a₂,a₃,a₄ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

E2: now

take c₁ = {0};
reconsider c₂ = 0 as Element of c₁ by TARSKI:def 1;
take c₃ = c₂;
deffunc H₁( Element of c₁, Element of c₁) -> Element of c₁ = c₃;
consider c₄ being BinOp of c₁ such that
E3: for b₁, b₂ being Element of c₁ holds c₄ . b₁,b₂ = H₁(b₁,b₂) from BINOP_1:sch 2();
deffunc H₂( Element of REAL , Element of c₁) -> Element of c₁ = c₃;
consider c₅ being Function of [:REAL ,c₁:],c₁ such that
E4: for b₁ being Element of REAL
for b₂ being Element of c₁ holds c₅ . [b₁,b₂] = H₂(b₁,b₂) from FUNCT_2:sch 8();
take c₆ = c₄;
take c₇ = c₅;
set c₈ = RLSStruct(# c₁,c₃,c₆,c₇ #);
thus for b₁, b₂ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ + b₂ = b₂ + b₁

proof

let c₉, c₁₀ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
E5: ( c₉ + c₁₀ = c₆ . c₉,c₁₀ & c₁₀ + c₉ = c₆ . c₁₀,c₉ ) ;
reconsider c₁₁ = c₉, c₁₂ = c₁₀ as Element of c₁ ;
( c₉ + c₁₀ = H₁(c₁₁,c₁₂) & c₁₀ + c₉ = H₁(c₁₂,c₁₁) ) by E3, E5;
hence c₉ + c₁₀ = c₁₀ + c₉ ;

end;

thus for b₁, b₂, b₃ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof

let c₉, c₁₀, c₁₁ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
E5: ( (c₉ + c₁₀) + c₁₁ = c₆ . (c₉ + c₁₀),c₁₁ & c₉ + (c₁₀ + c₁₁) = c₆ . c₉,(c₁₀ + c₁₁) ) ;
reconsider c₁₂ = c₉, c₁₃ = c₁₀, c₁₄ = c₁₁ as Element of c₁ ;
( (c₉ + c₁₀) + c₁₁ = H₁(H₁(c₁₂,c₁₃),c₁₄) & c₉ + (c₁₀ + c₁₁) = H₁(c₁₂,H₁(c₁₃,c₁₄)) ) by E3, E5;
hence (c₉ + c₁₀) + c₁₁ = c₉ + (c₁₀ + c₁₁) ;

end;

thus for b₁ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ + (0. RLSStruct(# c₁,c₃,c₆,c₇ #)) = b₁

proof

let c₉ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₉ as Element of c₁ ;
c₉ + (0. RLSStruct(# c₁,c₃,c₆,c₇ #)) = c₆ . [c₉,(0. RLSStruct(# c₁,c₃,c₆,c₇ #))]
.= c₆ . c₉,(0. RLSStruct(# c₁,c₃,c₆,c₇ #))
.= H₁(c₁₀,c₃) by E3 ;
hence c₉ + (0. RLSStruct(# c₁,c₃,c₆,c₇ #)) = c₉ by TARSKI:def 1;

end;

thus for b₁ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) ex b₂ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) st b₁ + b₂ = 0. RLSStruct(# c₁,c₃,c₆,c₇ #)

proof

let c₉ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₃ as VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) ;
take c₁₀ ;
thus c₉ + c₁₀ = c₆ . [c₉,c₁₀]
.= c₆ . c₉,c₁₀
.= the Zero of RLSStruct(# c₁,c₃,c₆,c₇ #) by E3
.= 0. RLSStruct(# c₁,c₃,c₆,c₇ #) ;

end;

thus for b₁ being Real
for b₂, b₃ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof

let c₉ be Real;
let c₁₀, c₁₁ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₂ = c₁₀, c₁₃ = c₁₁ as Element of c₁ ;
(c₉ * c₁₀) + (c₉ * c₁₁) = c₆ . [(c₉ * c₁₀),(c₉ * c₁₁)]
.= c₆ . (c₉ * c₁₀),(c₉ * c₁₁)
.= H₁(H₂(c₉,c₁₂),H₂(c₉,c₁₃)) by E3 ;
hence c₉ * (c₁₀ + c₁₁) = (c₉ * c₁₀) + (c₉ * c₁₁) by E4;

end;

thus for b₁, b₂ being Real
for b₃ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃)

proof

let c₉, c₁₀ be Real;
let c₁₁ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
set c₁₂ = c₉ + c₁₀;
reconsider c₁₃ = c₁₁ as Element of c₁ ;
E5: (c₉ + c₁₀) * c₁₁ = c₇ . [(c₉ + c₁₀),c₁₁]
.= H₂(c₉ + c₁₀,c₁₃) by E4 ;
(c₉ * c₁₁) + (c₁₀ * c₁₁) = c₆ . [(c₉ * c₁₁),(c₁₀ * c₁₁)]
.= c₆ . (c₉ * c₁₁),(c₁₀ * c₁₁)
.= H₁(H₂(c₉,c₁₃),H₂(c₁₀,c₁₃)) by E3 ;
hence (c₉ + c₁₀) * c₁₁ = (c₉ * c₁₁) + (c₁₀ * c₁₁) by E5;

end;

thus for b₁, b₂ being Real
for b₃ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof

let c₉, c₁₀ be Real;
let c₁₁ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
set c₁₂ = c₉ * c₁₀;
reconsider c₁₃ = c₁₁ as Element of c₁ ;
E5: (c₉ * c₁₀) * c₁₁ = c₇ . [(c₉ * c₁₀),c₁₁]
.= H₂(c₉ * c₁₀,c₁₃) by E4 ;
c₉ * (c₁₀ * c₁₁) = c₇ . [c₉,(c₁₀ * c₁₁)]
.= H₂(c₉,H₂(c₁₀,c₁₃)) by E4 ;
hence (c₉ * c₁₀) * c₁₁ = c₉ * (c₁₀ * c₁₁) by E5;

end;

thus for b₁ being VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #) holds 1 * b₁ = b₁

proof

let c₉ be VECTOR of RLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₉ as Element of c₁ ;
reconsider c₁₁ = 1 as Element of REAL ;
1 * c₉ = c₇ . [1,c₉]
.= H₂(c₁₁,c₁₀) by E4 ;
hence 1 * c₉ = c₉ by TARSKI:def 1;

end;

definition

let c₁ be non empty LoopStr ;
attr a₁ is Abelian means :Def5: :: RLVECT_1:def 5
for b₁, b₂ being Element of a₁ holds b₁ + b₂ = b₂ + b₁;
attr a₁ is add-associative means :Def6: :: RLVECT_1:def 6
for b₁, b₂, b₃ being Element of a₁ holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃);
attr a₁ is right_zeroed means :Def7: :: RLVECT_1:def 7
for b₁ being Element of a₁ holds b₁ + (0. a₁) = b₁;
attr a₁ is right_complementable means :Def8: :: RLVECT_1:def 8
for b₁ being Element of a₁ ex b₂ being Element of a₁ st b₁ + b₂ = 0. a₁;

end;

:: deftheorem Def5 defines Abelian RLVECT_1:def 5 :

:: deftheorem Def6 defines add-associative RLVECT_1:def 6 :

:: deftheorem Def7 defines right_zeroed RLVECT_1:def 7 :

:: deftheorem Def8 defines right_complementable RLVECT_1:def 8 :

definition

let c₁ be non empty RLSStruct ;
attr a₁ is RealLinearSpace-like means :Def9: :: RLVECT_1:def 9
( ( for b₁ being Real
for b₂, b₃ being VECTOR of a₁ holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) ) & ( for b₁, b₂ being Real
for b₃ being VECTOR of a₁ holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being Real
for b₃ being VECTOR of a₁ holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being VECTOR of a₁ holds 1 * b₁ = b₁ ) );

end;

:: deftheorem Def9 defines RealLinearSpace-like RLVECT_1:def 9 :

registration

cluster non empty strict Abelian add-associative right_zeroed right_complementable LoopStr ;
existence

proof end;

end;

registration

cluster non empty strict Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RLSStruct ;
existence

proof end;

end;

definition

mode RealLinearSpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RLSStruct ;

end;

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be Element of c₁;
redefine func + as c₂ + c₃ -> Element of a₁;
commutativity by Def5;

end;

theorem Th6: :: RLVECT_1:6

canceled;

theorem Th7: :: RLVECT_1:7

for b₁ being non empty RLSStruct st ( for b₂, b₃ being VECTOR of b₁ holds b₂ + b₃ = b₃ + b₂ ) & ( for b₂, b₃, b₄ being VECTOR of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂ being VECTOR of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being VECTOR of b₁ ex b₃ being VECTOR of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂ being Real
for b₃, b₄ being VECTOR of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) & ( for b₂, b₃ being Real
for b₄ being VECTOR of b₁ holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄) ) & ( for b₂, b₃ being Real
for b₄ being VECTOR of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being VECTOR of b₁ holds 1 * b₂ = b₂ ) holds
b₁ is RealLinearSpace by Def5, Def6, Def7, Def8, Def9;

Lemma8: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ holds
b₃ + b₂ = 0. b₁

proof end;

theorem Th8: :: RLVECT_1:8

canceled;

theorem Th9: :: RLVECT_1:9

canceled;

theorem Th10: :: RLVECT_1:10

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( b₂ + (0. b₁) = b₂ & (0. b₁) + b₂ = b₂ )

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be Element of c₁;
assume E10: ( c₁ is add-associative & c₁ is right_zeroed & c₁ is right_complementable ) ;
func - c₂ -> Element of a₁ means :Def10: :: RLVECT_1:def 10
a₂ + a₃ = 0. a₁;
existence by E10, Def8;
uniqueness

proof end;

end;

:: deftheorem Def10 defines - RLVECT_1:def 10 :

Lemma11: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₂ + b₄ = b₃

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Element of c₁;
func c₂ - c₃ -> Element of a₁ equals :: RLVECT_1:def 11
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def11 defines - RLVECT_1:def 11 :

theorem Th11: :: RLVECT_1:11

canceled;

theorem Th12: :: RLVECT_1:12

canceled;

theorem Th13: :: RLVECT_1:13

canceled;

theorem Th14: :: RLVECT_1:14

canceled;

theorem Th15: :: RLVECT_1:15

canceled;

theorem Th16: :: RLVECT_1:16

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( b₂ + (- b₂) = 0. b₁ & (- b₂) + b₂ = 0. b₁ )

proof end;

theorem Th17: :: RLVECT_1:17

canceled;

theorem Th18: :: RLVECT_1:18

canceled;

theorem Th19: :: RLVECT_1:19

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ holds
b₂ = - b₃

proof end;

theorem Th20: :: RLVECT_1:20

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₂ + b₄ = b₃ by Lemma11;

theorem Th21: :: RLVECT_1:21

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄, b₅ being Element of b₁ st ( b₂ + b₄ = b₂ + b₅ or b₄ + b₂ = b₅ + b₂ ) holds
b₄ = b₅

proof end;

theorem Th22: :: RLVECT_1:22

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st ( b₂ + b₃ = b₂ or b₃ + b₂ = b₂ ) holds
b₃ = 0. b₁

proof end;

theorem Th23: :: RLVECT_1:23

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ st ( b₁ = 0 or b₃ = 0. b₂ ) holds
b₁ * b₃ = 0. b₂

proof end;

theorem Th24: :: RLVECT_1:24

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds
( not b₁ * b₃ = 0. b₂ or b₁ = 0 or b₃ = 0. b₂ )

proof end;

theorem Th25: :: RLVECT_1:25

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr holds - (0. b₁) = 0. b₁

proof end;

theorem Th26: :: RLVECT_1:26

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds b₂ - (0. b₁) = b₂

proof end;

theorem Th27: :: RLVECT_1:27

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds (0. b₁) - b₂ = - b₂ by Th10;

theorem Th28: :: RLVECT_1:28

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds b₂ - b₂ = 0. b₁ by Def10;

theorem Th29: :: RLVECT_1:29

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds - b₂ = (- 1) * b₂

proof end;

theorem Th30: :: RLVECT_1:30

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds - (- b₂) = b₂

proof end;

theorem Th31: :: RLVECT_1:31

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st - b₂ = - b₃ holds
b₂ = b₃

proof end;

theorem Th32: :: RLVECT_1:32

canceled;

theorem Th33: :: RLVECT_1:33

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ st b₂ = - b₂ holds
b₂ = 0. b₁

proof end;

theorem Th34: :: RLVECT_1:34

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ st b₂ + b₂ = 0. b₁ holds
b₂ = 0. b₁

proof end;

theorem Th35: :: RLVECT_1:35

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ - b₃ = 0. b₁ holds
b₂ = b₃

proof end;

theorem Th36: :: RLVECT_1:36

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₃ - b₄ = b₂

proof end;

theorem Th37: :: RLVECT_1:37

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ - b₃ = b₂ - b₄ holds
b₃ = b₄

proof end;

theorem Th38: :: RLVECT_1:38

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds b₁ * (- b₃) = (- b₁) * b₃

proof end;

theorem Th39: :: RLVECT_1:39

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds b₁ * (- b₃) = - (b₁ * b₃)

proof end;

theorem Th40: :: RLVECT_1:40

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds (- b₁) * (- b₃) = b₁ * b₃

proof end;

Lemma27: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₂ + b₃) = (- b₃) + (- b₂)

proof end;

theorem Th41: :: RLVECT_1:41

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ - (b₃ + b₄) = (b₂ - b₄) - b₃

proof end;

theorem Th42: :: RLVECT_1:42

for b₁ being non empty add-associative LoopStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) - b₄ = b₂ + (b₃ - b₄) by Def6;

theorem Th43: :: RLVECT_1:43

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th44: :: RLVECT_1:44

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₂ + b₃) = (- b₃) - b₂

proof end;

theorem Th45: :: RLVECT_1:45

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₂ + b₃) = (- b₃) + (- b₂) by Lemma27;

theorem Th46: :: RLVECT_1:46

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds (- b₂) - b₃ = (- b₃) - b₂

proof end;

theorem Th47: :: RLVECT_1:47

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (b₂ - b₃) = b₃ + (- b₂)

proof end;

theorem Th48: :: RLVECT_1:48

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ holds b₁ * (b₃ - b₄) = (b₁ * b₃) - (b₁ * b₄)

proof end;

theorem Th49: :: RLVECT_1:49

for b₁, b₂ being Real
for b₃ being RealLinearSpace
for b₄ being VECTOR of b₃ holds (b₁ - b₂) * b₄ = (b₁ * b₄) - (b₂ * b₄)

proof end;

theorem Th50: :: RLVECT_1:50

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st b₁ <> 0 & b₁ * b₃ = b₁ * b₄ holds
b₃ = b₄

proof end;

theorem Th51: :: RLVECT_1:51

for b₁, b₂ being Real
for b₃ being RealLinearSpace
for b₄ being VECTOR of b₃ st b₄ <> 0. b₃ & b₁ * b₄ = b₂ * b₄ holds
b₁ = b₂

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃ be Element of c₁;
redefine func <* as <*c₂,c₃*> -> FinSequence of the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃, c₄ be Element of c₁;
redefine func <* as <*c₂,c₃,c₄*> -> FinSequence of the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty LoopStr ;
let c₂ be FinSequence of the carrier of c₁;
func Sum c₂ -> Element of a₁ means :Def12: :: RLVECT_1:def 12
ex b₁ being Function of NAT ,the carrier of a₁ st
( a₃ = b₁ . (len a₂) & b₁ . 0 = 0. a₁ & ( for b₂ being Nat
for b₃ being Element of a₁ st b₂ < len a₂ & b₃ = a₂ . (b₂ + 1) holds
b₁ . (b₂ + 1) = (b₁ . b₂) + b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Sum RLVECT_1:def 12 :

Lemma33: for b₁ being non empty LoopStr holds Sum (<*> the carrier of b₁) = 0. b₁

proof end;

Lemma34: for b₁ being non empty LoopStr
for b₂ being FinSequence of the carrier of b₁ st len b₂ = 0 holds
Sum b₂ = 0. b₁

proof end;

theorem Th52: :: RLVECT_1:52

canceled;

theorem Th53: :: RLVECT_1:53

canceled;

theorem Th54: :: RLVECT_1:54

for b₁ being non empty LoopStr
for b₂ being FinSequence of the carrier of b₁
for b₃, b₄ being Nat st b₃ in Seg b₄ & len b₂ = b₄ holds
b₂ . b₃ is Element of b₁

proof end;

theorem Th55: :: RLVECT_1:55

for b₁ being non empty LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Element of b₁ st len b₂ = (len b₃) + 1 & b₃ = b₂ | (dom b₃) & b₄ = b₂ . (len b₂) holds
Sum b₂ = (Sum b₃) + b₄

proof end;

theorem Th56: :: RLVECT_1:56

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄ being FinSequence of the carrier of b₂ st len b₃ = len b₄ & ( for b₅ being Nat
for b₆ being VECTOR of b₂ st b₅ in dom b₃ & b₆ = b₄ . b₅ holds
b₃ . b₅ = b₁ * b₆ ) holds
Sum b₃ = b₁ * (Sum b₄)

proof end;

theorem Th57: :: RLVECT_1:57

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st len b₂ = len b₃ & ( for b₄ being Nat
for b₅ being Element of b₁ st b₄ in dom b₂ & b₅ = b₃ . b₄ holds
b₂ . b₄ = - b₅ ) holds
Sum b₂ = - (Sum b₃)

proof end;

Lemma37: for b₁ being natural number st b₁ < 1 holds
b₁ = 0
by NAT_1:39;

theorem Th58: :: RLVECT_1:58

for b₁ being non empty add-associative right_zeroed LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ holds Sum (b₂ ^ b₃) = (Sum b₂) + (Sum b₃)

proof end;

Lemma39: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds Sum <*b₂*> = b₂

proof end;

theorem Th59: :: RLVECT_1:59

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st rng b₂ = rng b₃ & b₂ is one-to-one & b₃ is one-to-one holds
Sum b₂ = Sum b₃

proof end;

theorem Th60: :: RLVECT_1:60

for b₁ being non empty LoopStr holds Sum (<*> the carrier of b₁) = 0. b₁ by Lemma33;

theorem Th61: :: RLVECT_1:61

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds Sum <*b₂*> = b₂ by Lemma39;

theorem Th62: :: RLVECT_1:62

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*b₂,b₃*> = b₂ + b₃

proof end;

theorem Th63: :: RLVECT_1:63

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₂,b₃,b₄*> = (b₂ + b₃) + b₄

proof end;

theorem Th64: :: RLVECT_1:64

for b₁ being RealLinearSpace
for b₂ being Real holds b₂ * (Sum (<*> the carrier of b₁)) = 0. b₁

proof end;

theorem Th65: :: RLVECT_1:65

canceled;

theorem Th66: :: RLVECT_1:66

for b₁ being RealLinearSpace
for b₂ being Real
for b₃, b₄ being VECTOR of b₁ holds b₂ * (Sum <*b₃,b₄*>) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th67: :: RLVECT_1:67

for b₁ being RealLinearSpace
for b₂ being Real
for b₃, b₄, b₅ being VECTOR of b₁ holds b₂ * (Sum <*b₃,b₄,b₅*>) = ((b₂ * b₃) + (b₂ * b₄)) + (b₂ * b₅)

proof end;

theorem Th68: :: RLVECT_1:68

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr holds - (Sum (<*> the carrier of b₁)) = 0. b₁

proof end;

theorem Th69: :: RLVECT_1:69

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds - (Sum <*b₂*>) = - b₂ by Lemma39;

theorem Th70: :: RLVECT_1:70

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (Sum <*b₂,b₃*>) = (- b₂) - b₃

proof end;

theorem Th71: :: RLVECT_1:71

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds - (Sum <*b₂,b₃,b₄*>) = ((- b₂) - b₃) - b₄

proof end;

theorem Th72: :: RLVECT_1:72

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*b₂,b₃*> = Sum <*b₃,b₂*>

proof end;

theorem Th73: :: RLVECT_1:73

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*b₂,b₃*> = (Sum <*b₂*>) + (Sum <*b₃*>)

proof end;

theorem Th74: :: RLVECT_1:74

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr holds Sum <*(0. b₁),(0. b₁)*> = 0. b₁

proof end;

theorem Th75: :: RLVECT_1:75

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( Sum <*(0. b₁),b₂*> = b₂ & Sum <*b₂,(0. b₁)*> = b₂ )

proof end;

theorem Th76: :: RLVECT_1:76

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( Sum <*b₂,(- b₂)*> = 0. b₁ & Sum <*(- b₂),b₂*> = 0. b₁ )

proof end;

theorem Th77: :: RLVECT_1:77

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*b₂,(- b₃)*> = b₂ - b₃ by Th62;

theorem Th78: :: RLVECT_1:78

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds Sum <*(- b₂),(- b₃)*> = - (b₃ + b₂)

proof end;

theorem Th79: :: RLVECT_1:79

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*b₂,b₂*> = 2 * b₂

proof end;

theorem Th80: :: RLVECT_1:80

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*(- b₂),(- b₂)*> = (- 2) * b₂

proof end;

theorem Th81: :: RLVECT_1:81

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₂,b₃,b₄*> = ((Sum <*b₂*>) + (Sum <*b₃*>)) + (Sum <*b₄*>)

proof end;

theorem Th82: :: RLVECT_1:82

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₂,b₃,b₄*> = (Sum <*b₂,b₃*>) + b₄

proof end;

theorem Th83: :: RLVECT_1:83

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = (Sum <*b₂,b₄*>) + b₃

proof end;

theorem Th84: :: RLVECT_1:84

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = (Sum <*b₃,b₄*>) + b₂

proof end;

theorem Th85: :: RLVECT_1:85

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = Sum <*b₃,b₄,b₂*>

proof end;

theorem Th86: :: RLVECT_1:86

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = Sum <*b₂,b₃,b₄*>

proof end;

theorem Th87: :: RLVECT_1:87

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = Sum <*b₂,b₄,b₃*>

proof end;

theorem Th88: :: RLVECT_1:88

canceled;

theorem Th89: :: RLVECT_1:89

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds Sum <*b₃,b₂,b₄*> = Sum <*b₄,b₂,b₃*>

proof end;

theorem Th90: :: RLVECT_1:90

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr holds Sum <*(0. b₁),(0. b₁),(0. b₁)*> = 0. b₁

proof end;

theorem Th91: :: RLVECT_1:91

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds
( Sum <*(0. b₁),(0. b₁),b₂*> = b₂ & Sum <*(0. b₁),b₂,(0. b₁)*> = b₂ & Sum <*b₂,(0. b₁),(0. b₁)*> = b₂ )

proof end;

theorem Th92: :: RLVECT_1:92

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( Sum <*(0. b₁),b₂,b₃*> = b₂ + b₃ & Sum <*b₂,b₃,(0. b₁)*> = b₂ + b₃ & Sum <*b₂,(0. b₁),b₃*> = b₂ + b₃ )

proof end;

theorem Th93: :: RLVECT_1:93

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*b₂,b₂,b₂*> = 3 * b₂

proof end;

theorem Th94: :: RLVECT_1:94

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁ st len b₂ = 0 holds
Sum b₂ = 0. b₁ by Lemma34;

theorem Th95: :: RLVECT_1:95

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁ st len b₂ = 1 holds
Sum b₂ = b₂ . 1

proof end;

theorem Th96: :: RLVECT_1:96

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁
for b₃, b₄ being Element of b₁ st len b₂ = 2 & b₃ = b₂ . 1 & b₄ = b₂ . 2 holds
Sum b₂ = b₃ + b₄

proof end;

theorem Th97: :: RLVECT_1:97

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁
for b₃, b₄, b₅ being Element of b₁ st len b₂ = 3 & b₃ = b₂ . 1 & b₄ = b₂ . 2 & b₅ = b₂ . 3 holds
Sum b₂ = (b₃ + b₄) + b₅

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Element of c₁;
attr a₂ is non-zero means :: RLVECT_1:def 13
a₂ <> 0. a₁;

end;

:: deftheorem Def13 defines non-zero RLVECT_1:def 13 :