:: VECTSP_6 semantic presentation

definition
let c1 be non empty ZeroStr ;
let c2 be non empty VectSpStr of c1;
canceled;
canceled;
canceled;
mode Linear_Combination of c2 -> Element of Funcs the carrier of a2,the carrier of a1 means :Def4: :: VECTSP_6:def 4
ex b1 being finite Subset of a2 st
for b2 being Element of a2 st not b2 in b1 holds
a3 . b2 = 0. a1;
existence
ex b1 being Element of Funcs the carrier of c2,the carrier of c1ex b2 being finite Subset of c2 st
for b3 being Element of c2 st not b3 in b2 holds
b1 . b3 = 0. c1
proof end;
end;

:: deftheorem Def1 VECTSP_6:def 1 :
canceled;

:: deftheorem Def2 VECTSP_6:def 2 :
canceled;

:: deftheorem Def3 VECTSP_6:def 3 :
canceled;

:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
for b1 being non empty ZeroStr
for b2 being non empty VectSpStr of b1
for b3 being Element of Funcs the carrier of b2,the carrier of b1 holds
( b3 is Linear_Combination of b2 iff ex b4 being finite Subset of b2 st
for b5 being Element of b2 st not b5 in b4 holds
b3 . b5 = 0. b1 );

definition
let c1 be non empty ZeroStr ;
let c2 be non empty VectSpStr of c1;
let c3 be Linear_Combination of c2;
func Carrier c3 -> finite Subset of a2 equals :: VECTSP_6:def 5
{ b1 where B is Element of a2 : a3 . b1 <> 0. a1 } ;
coherence
{ b1 where B is Element of c2 : c3 . b1 <> 0. c1 } is finite Subset of c2
proof end;
end;

:: deftheorem Def5 defines Carrier VECTSP_6:def 5 :
for b1 being non empty ZeroStr
for b2 being non empty VectSpStr of b1
for b3 being Linear_Combination of b2 holds Carrier b3 = { b4 where B is Element of b2 : b3 . b4 <> 0. b1 } ;

theorem Th1: :: VECTSP_6:1
canceled;

theorem Th2: :: VECTSP_6:2
canceled;

theorem Th3: :: VECTSP_6:3
canceled;

theorem Th4: :: VECTSP_6:4
canceled;

theorem Th5: :: VECTSP_6:5
canceled;

theorem Th6: :: VECTSP_6:6
canceled;

theorem Th7: :: VECTSP_6:7
canceled;

theorem Th8: :: VECTSP_6:8
canceled;

theorem Th9: :: VECTSP_6:9
canceled;

theorem Th10: :: VECTSP_6:10
canceled;

theorem Th11: :: VECTSP_6:11
canceled;

theorem Th12: :: VECTSP_6:12
canceled;

theorem Th13: :: VECTSP_6:13
canceled;

theorem Th14: :: VECTSP_6:14
canceled;

theorem Th15: :: VECTSP_6:15
canceled;

theorem Th16: :: VECTSP_6:16
canceled;

theorem Th17: :: VECTSP_6:17
canceled;

theorem Th18: :: VECTSP_6:18
canceled;

theorem Th19: :: VECTSP_6:19
for b1 being set
for b2 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b3 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b2
for b4 being Linear_Combination of b3 holds
( b1 in Carrier b4 iff ex b5 being Element of b3 st
( b1 = b5 & b4 . b5 <> 0. b2 ) ) ;

theorem Th20: :: VECTSP_6:20
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4 being Linear_Combination of b2 holds
( b4 . b3 = 0. b1 iff not b3 in Carrier b4 )
proof end;

definition
let c1 be non empty ZeroStr ;
let c2 be non empty VectSpStr of c1;
func ZeroLC c2 -> Linear_Combination of a2 means :Def6: :: VECTSP_6:def 6
Carrier a3 = {} ;
existence
ex b1 being Linear_Combination of c2 st Carrier b1 = {}
proof end;
uniqueness
for b1, b2 being Linear_Combination of c2 st Carrier b1 = {} & Carrier b2 = {} holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :
for b1 being non empty ZeroStr
for b2 being non empty VectSpStr of b1
for b3 being Linear_Combination of b2 holds
( b3 = ZeroLC b2 iff Carrier b3 = {} );

theorem Th21: :: VECTSP_6:21
canceled;

theorem Th22: :: VECTSP_6:22
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2 holds (ZeroLC b2) . b3 = 0. b1
proof end;

definition
let c1 be non empty ZeroStr ;
let c2 be non empty VectSpStr of c1;
let c3 be Subset of c2;
mode Linear_Combination of c3 -> Linear_Combination of a2 means :Def7: :: VECTSP_6:def 7
Carrier a4 c= a3;
existence
ex b1 being Linear_Combination of c2 st Carrier b1 c= c3
proof end;
end;

:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :
for b1 being non empty ZeroStr
for b2 being non empty VectSpStr of b1
for b3 being Subset of b2
for b4 being Linear_Combination of b2 holds
( b4 is Linear_Combination of b3 iff Carrier b4 c= b3 );

theorem Th23: :: VECTSP_6:23
canceled;

theorem Th24: :: VECTSP_6:24
canceled;

theorem Th25: :: VECTSP_6:25
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Subset of b2
for b5 being Linear_Combination of b3 st b3 c= b4 holds
b5 is Linear_Combination of b4
proof end;

theorem Th26: :: VECTSP_6:26
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Subset of b2 holds ZeroLC b2 is Linear_Combination of b3
proof end;

theorem Th27: :: VECTSP_6:27
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of {} the carrier of b2 holds b3 = ZeroLC b2
proof end;

theorem Th28: :: VECTSP_6:28
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds b3 is Linear_Combination of Carrier b3 by Def7;

definition
let c1 be non empty LoopStr ;
let c2 be non empty VectSpStr of c1;
let c3 be FinSequence of the carrier of c2;
let c4 be Function of the carrier of c2,the carrier of c1;
func c4 (#) c3 -> FinSequence of the carrier of a2 means :Def8: :: VECTSP_6:def 8
( len a5 = len a3 & ( for b1 being Nat st b1 in dom a5 holds
a5 . b1 = (a4 . (a3 /. b1)) * (a3 /. b1) ) );
existence
ex b1 being FinSequence of the carrier of c2 st
( len b1 = len c3 & ( for b2 being Nat st b2 in dom b1 holds
b1 . b2 = (c4 . (c3 /. b2)) * (c3 /. b2) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of c2 st len b1 = len c3 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 = (c4 . (c3 /. b3)) * (c3 /. b3) ) & len b2 = len c3 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 = (c4 . (c3 /. b3)) * (c3 /. b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines (#) VECTSP_6:def 8 :
for b1 being non empty LoopStr
for b2 being non empty VectSpStr of b1
for b3 being FinSequence of the carrier of b2
for b4 being Function of the carrier of b2,the carrier of b1
for b5 being FinSequence of the carrier of b2 holds
( b5 = b4 (#) b3 iff ( len b5 = len b3 & ( for b6 being Nat st b6 in dom b5 holds
b5 . b6 = (b4 . (b3 /. b6)) * (b3 /. b6) ) ) );

theorem Th29: :: VECTSP_6:29
canceled;

theorem Th30: :: VECTSP_6:30
canceled;

theorem Th31: :: VECTSP_6:31
canceled;

theorem Th32: :: VECTSP_6:32
for b1 being Nat
for b2 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b3 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b2
for b4 being Element of b3
for b5 being FinSequence of the carrier of b3
for b6 being Function of the carrier of b3,the carrier of b2 st b1 in dom b5 & b4 = b5 . b1 holds
(b6 (#) b5) . b1 = (b6 . b4) * b4
proof end;

theorem Th33: :: VECTSP_6:33
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Function of the carrier of b2,the carrier of b1 holds b3 (#) (<*> the carrier of b2) = <*> the carrier of b2
proof end;

theorem Th34: :: VECTSP_6:34
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4 being Function of the carrier of b2,the carrier of b1 holds b4 (#) <*b3*> = <*((b4 . b3) * b3)*>
proof end;

theorem Th35: :: VECTSP_6:35
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Element of b2
for b5 being Function of the carrier of b2,the carrier of b1 holds b5 (#) <*b3,b4*> = <*((b5 . b3) * b3),((b5 . b4) * b4)*>
proof end;

theorem Th36: :: VECTSP_6:36
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4, b5 being Element of b2
for b6 being Function of the carrier of b2,the carrier of b1 holds b6 (#) <*b3,b4,b5*> = <*((b6 . b3) * b3),((b6 . b4) * b4),((b6 . b5) * b5)*>
proof end;

theorem Th37: :: VECTSP_6:37
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being FinSequence of the carrier of b2
for b5 being Function of the carrier of b2,the carrier of b1 holds b5 (#) (b3 ^ b4) = (b5 (#) b3) ^ (b5 (#) b4)
proof end;

definition
let c1 be non empty LoopStr ;
let c2 be non empty VectSpStr of c1;
let c3 be Linear_Combination of c2;
assume E12: ( c2 is Abelian & c2 is add-associative & c2 is right_zeroed & c2 is right_complementable ) ;
func Sum c3 -> Element of a2 means :Def9: :: VECTSP_6:def 9
ex b1 being FinSequence of the carrier of a2 st
( b1 is one-to-one & rng b1 = Carrier a3 & a4 = Sum (a3 (#) b1) );
existence
ex b1 being Element of c2ex b2 being FinSequence of the carrier of c2 st
( b2 is one-to-one & rng b2 = Carrier c3 & b1 = Sum (c3 (#) b2) )
proof end;
uniqueness
for b1, b2 being Element of c2 st ex b3 being FinSequence of the carrier of c2 st
( b3 is one-to-one & rng b3 = Carrier c3 & b1 = Sum (c3 (#) b3) ) & ex b3 being FinSequence of the carrier of c2 st
( b3 is one-to-one & rng b3 = Carrier c3 & b2 = Sum (c3 (#) b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Sum VECTSP_6:def 9 :
for b1 being non empty LoopStr
for b2 being non empty VectSpStr of b1
for b3 being Linear_Combination of b2 st b2 is Abelian & b2 is add-associative & b2 is right_zeroed & b2 is right_complementable holds
for b4 being Element of b2 holds
( b4 = Sum b3 iff ex b5 being FinSequence of the carrier of b2 st
( b5 is one-to-one & rng b5 = Carrier b3 & b4 = Sum (b3 (#) b5) ) );

Lemma13: for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1 holds Sum (ZeroLC b2) = 0. b2
proof end;

theorem Th38: :: VECTSP_6:38
canceled;

theorem Th39: :: VECTSP_6:39
canceled;

theorem Th40: :: VECTSP_6:40
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Subset of b2 st 0. b1 <> 1. b1 holds
( ( b3 <> {} & b3 is lineary-closed ) iff for b4 being Linear_Combination of b3 holds Sum b4 in b3 )
proof end;

theorem Th41: :: VECTSP_6:41
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1 holds Sum (ZeroLC b2) = 0. b2 by Lemma13;

theorem Th42: :: VECTSP_6:42
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of {} the carrier of b2 holds Sum b3 = 0. b2
proof end;

theorem Th43: :: VECTSP_6:43
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4 being Linear_Combination of {b3} holds Sum b4 = (b4 . b3) * b3
proof end;

theorem Th44: :: VECTSP_6:44
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Element of b2 st b3 <> b4 holds
for b5 being Linear_Combination of {b3,b4} holds Sum b5 = ((b5 . b3) * b3) + ((b5 . b4) * b4)
proof end;

theorem Th45: :: VECTSP_6:45
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 st Carrier b3 = {} holds
Sum b3 = 0. b2
proof end;

theorem Th46: :: VECTSP_6:46
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4 being Linear_Combination of b2 st Carrier b4 = {b3} holds
Sum b4 = (b4 . b3) * b3
proof end;

theorem Th47: :: VECTSP_6:47
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Element of b2
for b5 being Linear_Combination of b2 st Carrier b5 = {b3,b4} & b3 <> b4 holds
Sum b5 = ((b5 . b3) * b3) + ((b5 . b4) * b4)
proof end;

definition
let c1 be non empty ZeroStr ;
let c2 be non empty VectSpStr of c1;
let c3, c4 be Linear_Combination of c2;
redefine pred = as c3 = c4 means :: VECTSP_6:def 10
for b1 being Element of a2 holds a3 . b1 = a4 . b1;
compatibility
( c3 = c4 iff for b1 being Element of c2 holds c3 . b1 = c4 . b1 )
by FUNCT_2:113;
end;

:: deftheorem Def10 defines = VECTSP_6:def 10 :
for b1 being non empty ZeroStr
for b2 being non empty VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds
( b3 = b4 iff for b5 being Element of b2 holds b3 . b5 = b4 . b5 );

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c2 be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c1;
let c3, c4 be Linear_Combination of c2;
func c3 + c4 -> Linear_Combination of a2 means :Def11: :: VECTSP_6:def 11
for b1 being Element of a2 holds a5 . b1 = (a3 . b1) + (a4 . b1);
existence
ex b1 being Linear_Combination of c2 st
for b2 being Element of c2 holds b1 . b2 = (c3 . b2) + (c4 . b2)
proof end;
uniqueness
for b1, b2 being Linear_Combination of c2 st ( for b3 being Element of c2 holds b1 . b3 = (c3 . b3) + (c4 . b3) ) & ( for b3 being Element of c2 holds b2 . b3 = (c3 . b3) + (c4 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines + VECTSP_6:def 11 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4, b5 being Linear_Combination of b2 holds
( b5 = b3 + b4 iff for b6 being Element of b2 holds b5 . b6 = (b3 . b6) + (b4 . b6) );

theorem Th48: :: VECTSP_6:48
canceled;

theorem Th49: :: VECTSP_6:49
canceled;

theorem Th50: :: VECTSP_6:50
canceled;

theorem Th51: :: VECTSP_6:51
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds Carrier (b3 + b4) c= (Carrier b3) \/ (Carrier b4)
proof end;

theorem Th52: :: VECTSP_6:52
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Subset of b2
for b4, b5 being Linear_Combination of b2 st b4 is Linear_Combination of b3 & b5 is Linear_Combination of b3 holds
b4 + b5 is Linear_Combination of b3
proof end;

theorem Th53: :: VECTSP_6:53
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds b3 + b4 = b4 + b3
proof end;

theorem Th54: :: VECTSP_6:54
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4, b5 being Linear_Combination of b2 holds b3 + (b4 + b5) = (b3 + b4) + b5
proof end;

theorem Th55: :: VECTSP_6:55
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds
( b3 + (ZeroLC b2) = b3 & (ZeroLC b2) + b3 = b3 )
proof end;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c2 be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c1;
let c3 be Element of c1;
let c4 be Linear_Combination of c2;
func c3 * c4 -> Linear_Combination of a2 means :Def12: :: VECTSP_6:def 12
for b1 being Element of a2 holds a5 . b1 = a3 * (a4 . b1);
existence
ex b1 being Linear_Combination of c2 st
for b2 being Element of c2 holds b1 . b2 = c3 * (c4 . b2)
proof end;
uniqueness
for b1, b2 being Linear_Combination of c2 st ( for b3 being Element of c2 holds b1 . b3 = c3 * (c4 . b3) ) & ( for b3 being Element of c2 holds b2 . b3 = c3 * (c4 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines * VECTSP_6:def 12 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4, b5 being Linear_Combination of b2 holds
( b5 = b3 * b4 iff for b6 being Element of b2 holds b5 . b6 = b3 * (b4 . b6) );

theorem Th56: :: VECTSP_6:56
canceled;

theorem Th57: :: VECTSP_6:57
canceled;

theorem Th58: :: VECTSP_6:58
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4 being Linear_Combination of b2 holds Carrier (b3 * b4) c= Carrier b4
proof end;

theorem Th59: :: VECTSP_6:59
for b1 being Field
for b2 being VectSp of b1
for b3 being Element of b1
for b4 being Linear_Combination of b2 st b3 <> 0. b1 holds
Carrier (b3 * b4) = Carrier b4
proof end;

theorem Th60: :: VECTSP_6:60
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds (0. b1) * b3 = ZeroLC b2
proof end;

theorem Th61: :: VECTSP_6:61
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4 being Subset of b2
for b5 being Linear_Combination of b2 st b5 is Linear_Combination of b4 holds
b3 * b5 is Linear_Combination of b4
proof end;

theorem Th62: :: VECTSP_6:62
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Element of b1
for b5 being Linear_Combination of b2 holds (b3 + b4) * b5 = (b3 * b5) + (b4 * b5)
proof end;

theorem Th63: :: VECTSP_6:63
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b1
for b4, b5 being Linear_Combination of b2 holds b3 * (b4 + b5) = (b3 * b4) + (b3 * b5)
proof end;

theorem Th64: :: VECTSP_6:64
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Element of b1
for b5 being Linear_Combination of b2 holds b3 * (b4 * b5) = (b3 * b4) * b5
proof end;

theorem Th65: :: VECTSP_6:65
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds (1. b1) * b3 = b3
proof end;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c2 be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c1;
let c3 be Linear_Combination of c2;
func - c3 -> Linear_Combination of a2 equals :: VECTSP_6:def 13
(- (1. a1)) * a3;
correctness
coherence
(- (1. c1)) * c3 is Linear_Combination of c2
;
;
involutiveness
for b1, b2 being Linear_Combination of c2 st b1 = (- (1. c1)) * b2 holds
b2 = (- (1. c1)) * b1
proof end;
end;

:: deftheorem Def13 defines - VECTSP_6:def 13 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds - b3 = (- (1. b1)) * b3;

Lemma26: for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being Element of b1 holds (- (1. b1)) * b2 = - b2
proof end;

theorem Th66: :: VECTSP_6:66
canceled;

theorem Th67: :: VECTSP_6:67
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4 being Linear_Combination of b2 holds (- b4) . b3 = - (b4 . b3)
proof end;

theorem Th68: :: VECTSP_6:68
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 st b3 + b4 = ZeroLC b2 holds
b4 = - b3
proof end;

Lemma28: for b1 being Field holds - (1. b1) <> 0. b1
proof end;

Lemma29: for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds Carrier (- b3) c= Carrier b3
by Th58;

theorem Th69: :: VECTSP_6:69
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds Carrier (- b3) = Carrier b3
proof end;

theorem Th70: :: VECTSP_6:70
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Subset of b2
for b4 being Linear_Combination of b2 st b4 is Linear_Combination of b3 holds
- b4 is Linear_Combination of b3 by Th61;

definition
let c1 be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c2 be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c1;
let c3, c4 be Linear_Combination of c2;
func c3 - c4 -> Linear_Combination of a2 equals :: VECTSP_6:def 14
a3 + (- a4);
coherence
c3 + (- c4) is Linear_Combination of c2
;
end;

:: deftheorem Def14 defines - VECTSP_6:def 14 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds b3 - b4 = b3 + (- b4);

theorem Th71: :: VECTSP_6:71
canceled;

theorem Th72: :: VECTSP_6:72
canceled;

theorem Th73: :: VECTSP_6:73
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Element of b2
for b4, b5 being Linear_Combination of b2 holds (b4 - b5) . b3 = (b4 . b3) - (b5 . b3)
proof end;

theorem Th74: :: VECTSP_6:74
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds Carrier (b3 - b4) c= (Carrier b3) \/ (Carrier b4)
proof end;

theorem Th75: :: VECTSP_6:75
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Subset of b2
for b4, b5 being Linear_Combination of b2 st b4 is Linear_Combination of b3 & b5 is Linear_Combination of b3 holds
b4 - b5 is Linear_Combination of b3
proof end;

theorem Th76: :: VECTSP_6:76
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds b3 - b3 = ZeroLC b2
proof end;

theorem Th77: :: VECTSP_6:77
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds Sum (b3 + b4) = (Sum b3) + (Sum b4)
proof end;

theorem Th78: :: VECTSP_6:78
for b1 being Field
for b2 being VectSp of b1
for b3 being Linear_Combination of b2
for b4 being Element of b1 holds Sum (b4 * b3) = b4 * (Sum b3)
proof end;

theorem Th79: :: VECTSP_6:79
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds Sum (- b3) = - (Sum b3)
proof end;

theorem Th80: :: VECTSP_6:80
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3, b4 being Linear_Combination of b2 holds Sum (b3 - b4) = (Sum b3) - (Sum b4)
proof end;

theorem Th81: :: VECTSP_6:81
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being Element of b1 holds (- (1. b1)) * b2 = - b2 by Lemma26;

theorem Th82: :: VECTSP_6:82
for b1 being Field holds - (1. b1) <> 0. b1 by Lemma28;