:: VECTSP_4 semantic presentation

Lemma1: for b1 being non empty Abelian add-associative right_zeroed right_complementable associative commutative 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 Element of b2 holds (b3 - b4) * b5 = (b3 * b5) - (b4 * b5)
proof end;

definition
let c1 be non empty HGrStr ;
let c2 be non empty VectSpStr of c1;
let c3 be Subset of c2;
attr a3 is lineary-closed means :Def1: :: VECTSP_4:def 1
( ( for b1, b2 being Element of a2 st b1 in a3 & b2 in a3 holds
b1 + b2 in a3 ) & ( for b1 being Element of a1
for b2 being Element of a2 st b2 in a3 holds
b1 * b2 in a3 ) );
end;

:: deftheorem Def1 defines lineary-closed VECTSP_4:def 1 :
for b1 being non empty HGrStr
for b2 being non empty VectSpStr of b1
for b3 being Subset of b2 holds
( b3 is lineary-closed iff ( ( for b4, b5 being Element of b2 st b4 in b3 & b5 in b3 holds
b4 + b5 in b3 ) & ( for b4 being Element of b1
for b5 being Element of b2 st b5 in b3 holds
b4 * b5 in b3 ) ) );

theorem Th1: :: VECTSP_4:1
canceled;

theorem Th2: :: VECTSP_4:2
canceled;

theorem Th3: :: VECTSP_4:3
canceled;

theorem Th4: :: VECTSP_4:4
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 b3 <> {} & b3 is lineary-closed holds
0. b2 in b3
proof end;

theorem Th5: :: VECTSP_4:5
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 b3 is lineary-closed holds
for b4 being Element of b2 st b4 in b3 holds
- b4 in b3
proof end;

theorem Th6: :: VECTSP_4:6
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 b3 is lineary-closed holds
for b4, b5 being Element of b2 st b4 in b3 & b5 in b3 holds
b4 - b5 in b3
proof end;

theorem Th7: :: VECTSP_4:7
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 {(0. b2)} is lineary-closed
proof end;

theorem Th8: :: VECTSP_4:8
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 the carrier of b2 = b3 holds
b3 is lineary-closed
proof end;

theorem Th9: :: VECTSP_4:9
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 Subset of b2 st b3 is lineary-closed & b4 is lineary-closed & b5 = { (b6 + b7) where B is Element of b2, B is Element of b2 : ( b6 in b3 & b7 in b4 ) } holds
b5 is lineary-closed
proof end;

theorem Th10: :: VECTSP_4:10
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 st b3 is lineary-closed & b4 is lineary-closed holds
b3 /\ b4 is lineary-closed
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;
mode Subspace of c2 -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of a1 means :Def2: :: VECTSP_4:def 2
( the carrier of a3 c= the carrier of a2 & the Zero of a3 = the Zero of a2 & the add of a3 = the add of a2 || the carrier of a3 & the lmult of a3 = the lmult of a2 | [:the carrier of a1,the carrier of a3:] );
existence
ex b1 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c1 st
( the carrier of b1 c= the carrier of c2 & the Zero of b1 = the Zero of c2 & the add of b1 = the add of c2 || the carrier of b1 & the lmult of b1 = the lmult of c2 | [:the carrier of c1,the carrier of b1:] )
proof end;
end;

:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2, b3 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1 holds
( b3 is Subspace of b2 iff ( the carrier of b3 c= the carrier of b2 & the Zero of b3 = the Zero of b2 & the add of b3 = the add of b2 || the carrier of b3 & the lmult of b3 = the lmult of b2 | [:the carrier of b1,the carrier of b3:] ) );

theorem Th11: :: VECTSP_4:11
canceled;

theorem Th12: :: VECTSP_4:12
canceled;

theorem Th13: :: VECTSP_4:13
canceled;

theorem Th14: :: VECTSP_4:14
canceled;

theorem Th15: :: VECTSP_4:15
canceled;

theorem Th16: :: VECTSP_4:16
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, b5 being Subspace of b3 st b1 in b4 & b4 is Subspace of b5 holds
b1 in b5
proof end;

theorem Th17: :: VECTSP_4:17
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 Subspace of b3 st b1 in b4 holds
b1 in b3
proof end;

theorem Th18: :: VECTSP_4:18
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 Subspace of b2
for b4 being Element of b3 holds b4 is Element of b2
proof end;

theorem Th19: :: VECTSP_4:19
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 Subspace of b2 holds 0. b3 = 0. b2 by Def2;

theorem Th20: :: VECTSP_4: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, b4 being Subspace of b2 holds 0. b3 = 0. b4
proof end;

theorem Th21: :: VECTSP_4:21
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 Subspace of b2
for b6, b7 being Element of b5 st b6 = b3 & b7 = b4 holds
b6 + b7 = b3 + b4
proof end;

theorem Th22: :: VECTSP_4: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 b1
for b4 being Element of b2
for b5 being Subspace of b2
for b6 being Element of b5 st b6 = b4 holds
b3 * b6 = b3 * b4
proof end;

theorem Th23: :: VECTSP_4:23
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 Subspace of b2
for b5 being Element of b4 st b5 = b3 holds
- b3 = - b5
proof end;

theorem Th24: :: VECTSP_4:24
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 Subspace of b2
for b6, b7 being Element of b5 st b6 = b3 & b7 = b4 holds
b6 - b7 = b3 - b4
proof end;

Lemma14: 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 Subspace of b2
for b4 being Subset of b2 st the carrier of b3 = b4 holds
b4 is lineary-closed
proof end;

theorem Th25: :: VECTSP_4: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 being Subspace of b2 holds 0. b2 in b3
proof end;

theorem Th26: :: VECTSP_4: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, b4 being Subspace of b2 holds 0. b3 in b4
proof end;

theorem Th27: :: VECTSP_4: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 Subspace of b2 holds 0. b3 in b2
proof end;

theorem Th28: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 st b3 in b5 & b4 in b5 holds
b3 + b4 in b5
proof end;

theorem Th29: :: VECTSP_4:29
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 Element of b2
for b5 being Subspace of b2 st b4 in b5 holds
b3 * b4 in b5
proof end;

theorem Th30: :: VECTSP_4:30
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 Subspace of b2 st b3 in b4 holds
- b3 in b4
proof end;

theorem Th31: :: VECTSP_4:31
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 Subspace of b2 st b3 in b5 & b4 in b5 holds
b3 - b4 in b5
proof end;

theorem Th32: :: VECTSP_4:32
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 b2 is Subspace of b2
proof end;

theorem Th33: :: VECTSP_4:33
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2, b3 being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of b1 st b3 is Subspace of b2 & b2 is Subspace of b3 holds
b3 = b2
proof end;

theorem Th34: :: VECTSP_4:34
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2, b3, b4 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1 st b2 is Subspace of b3 & b3 is Subspace of b4 holds
b2 is Subspace of b4
proof end;

theorem Th35: :: VECTSP_4: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 Subspace of b2 st the carrier of b3 c= the carrier of b4 holds
b3 is Subspace of b4
proof end;

theorem Th36: :: VECTSP_4: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 being Subspace of b2 st ( for b5 being Element of b2 st b5 in b3 holds
b5 in b4 ) holds
b3 is Subspace of b4
proof end;

registration
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;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like Subspace of a2;
existence
ex b1 being Subspace of c2 st b1 is strict
proof end;
end;

theorem Th37: :: VECTSP_4: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 strict Subspace of b2 st the carrier of b3 = the carrier of b4 holds
b3 = b4
proof end;

theorem Th38: :: VECTSP_4:38
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 strict Subspace of b2 st ( for b5 being Element of b2 holds
( b5 in b3 iff b5 in b4 ) ) holds
b3 = b4
proof end;

theorem Th39: :: VECTSP_4:39
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 strict VectSp-like VectSpStr of b1
for b3 being strict Subspace of b2 st the carrier of b3 = the carrier of b2 holds
b3 = b2
proof end;

theorem Th40: :: VECTSP_4: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 strict VectSp-like VectSpStr of b1
for b3 being strict Subspace of b2 st ( for b4 being Element of b2 holds b4 in b3 ) holds
b3 = b2
proof end;

theorem Th41: :: VECTSP_4: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
for b3 being Subspace of b2
for b4 being Subset of b2 st the carrier of b3 = b4 holds
b4 is lineary-closed by Lemma14;

theorem Th42: :: VECTSP_4: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 Subset of b2 st b3 <> {} & b3 is lineary-closed holds
ex b4 being strict Subspace of b2 st b3 = the carrier of b4
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;
func (0). c2 -> strict Subspace of a2 means :Def3: :: VECTSP_4:def 3
the carrier of a3 = {(0. a2)};
correctness
existence
ex b1 being strict Subspace of c2 st the carrier of b1 = {(0. c2)};
uniqueness
for b1, b2 being strict Subspace of c2 st the carrier of b1 = {(0. c2)} & the carrier of b2 = {(0. c2)} holds
b1 = b2;
proof end;
end;

:: deftheorem Def3 defines (0). VECTSP_4:def 3 :
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 strict Subspace of b2 holds
( b3 = (0). b2 iff the carrier of b3 = {(0. b2)} );

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;
func (Omega). c2 -> strict Subspace of a2 equals :: VECTSP_4:def 4
 VectSpStr(# the carrier of a2,the add of a2,the Zero of a2,the lmult of a2 #);
coherence
VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,the lmult of c2 #) is strict Subspace of c2
proof end;
end;

:: deftheorem Def4 defines (Omega). VECTSP_4:def 4 :
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 (Omega). b2 = VectSpStr(# the carrier of b2,the add of b2,the Zero of b2,the lmult of b2 #);

theorem Th43: :: VECTSP_4:43
canceled;

theorem Th44: :: VECTSP_4:44
canceled;

theorem Th45: :: VECTSP_4:45
canceled;

theorem Th46: :: VECTSP_4:46
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 holds
( b1 in (0). b3 iff b1 = 0. b3 )
proof end;

theorem Th47: :: VECTSP_4: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 being Subspace of b2 holds (0). b3 = (0). b2
proof end;

theorem Th48: :: VECTSP_4:48
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 Subspace of b2 holds (0). b3 = (0). b4
proof end;

theorem Th49: :: VECTSP_4:49
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 Subspace of b2 holds (0). b3 is Subspace of b2 by Th34;

theorem Th50: :: VECTSP_4:50
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 Subspace of b2 holds (0). b2 is Subspace of b3
proof end;

theorem Th51: :: VECTSP_4: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 Subspace of b2 holds (0). b3 is Subspace of b4
proof end;

theorem Th52: :: VECTSP_4:52
canceled;

theorem Th53: :: VECTSP_4: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 strict VectSp-like VectSpStr of b1 holds b2 is Subspace of (Omega). b2 ;

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 c2;
let c4 be Subspace of c2;
func c3 + c4 -> Subset of a2 equals :: VECTSP_4:def 5
{ (a3 + b1) where B is Element of a2 : b1 in a4 } ;
coherence
{ (c3 + b1) where B is Element of c2 : b1 in c4 } is Subset of c2
proof end;
end;

:: deftheorem Def5 defines + VECTSP_4:def 5 :
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 Subspace of b2 holds b3 + b4 = { (b3 + b5) where B is Element of b2 : b5 in b4 } ;

Lemma30: 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 Subspace of b2 holds (0. b2) + b3 = the carrier of 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 Subspace of c2;
mode Coset of c3 -> Subset of a2 means :Def6: :: VECTSP_4:def 6
ex b1 being Element of a2 st a4 = b1 + a3;
existence
ex b1 being Subset of c2ex b2 being Element of c2 st b1 = b2 + c3
proof end;
end;

:: deftheorem Def6 defines Coset VECTSP_4:def 6 :
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 Subspace of b2
for b4 being Subset of b2 holds
( b4 is Coset of b3 iff ex b5 being Element of b2 st b4 = b5 + b3 );

theorem Th54: :: VECTSP_4:54
canceled;

theorem Th55: :: VECTSP_4:55
canceled;

theorem Th56: :: VECTSP_4:56
canceled;

theorem Th57: :: VECTSP_4:57
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 Element of b3
for b5 being Subspace of b3 holds
( b1 in b4 + b5 iff ex b6 being Element of b3 st
( b6 in b5 & b1 = b4 + b6 ) )
proof end;

theorem Th58: :: VECTSP_4: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 b2
for b4 being Subspace of b2 holds
( 0. b2 in b3 + b4 iff b3 in b4 )
proof end;

theorem Th59: :: VECTSP_4:59
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 Subspace of b2 holds b3 in b3 + b4
proof end;

theorem Th60: :: VECTSP_4: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 Subspace of b2 holds (0. b2) + b3 = the carrier of b3 by Lemma30;

theorem Th61: :: VECTSP_4: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 b2 holds b3 + ((0). b2) = {b3}
proof end;

Lemma36: 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 Subspace of b2 holds
( b3 in b4 iff b3 + b4 = the carrier of b4 )
proof end;

theorem Th62: :: VECTSP_4: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 being Element of b2 holds b3 + ((Omega). b2) = the carrier of b2
proof end;

theorem Th63: :: VECTSP_4: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 b2
for b4 being Subspace of b2 holds
( 0. b2 in b3 + b4 iff b3 + b4 = the carrier of b4 )
proof end;

theorem Th64: :: VECTSP_4: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 being Element of b2
for b4 being Subspace of b2 holds
( b3 in b4 iff b3 + b4 = the carrier of b4 ) by Lemma36;

theorem Th65: :: VECTSP_4: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 Element of b1
for b4 being Element of b2
for b5 being Subspace of b2 st b4 in b5 holds
(b3 * b4) + b5 = the carrier of b5
proof end;

theorem Th66: :: VECTSP_4:66
for b1 being Field
for b2 being VectSp of b1
for b3 being Element of b1
for b4 being Element of b2
for b5 being Subspace of b2 st b3 <> 0. b1 & (b3 * b4) + b5 = the carrier of b5 holds
b4 in b5
proof end;

theorem Th67: :: VECTSP_4:67
for b1 being Field
for b2 being VectSp of b1
for b3 being Element of b2
for b4 being Subspace of b2 holds
( b3 in b4 iff (- b3) + b4 = the carrier of b4 )
proof end;

theorem Th68: :: VECTSP_4: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 Element of b2
for b5 being Subspace of b2 holds
( b3 in b5 iff b4 + b5 = (b4 + b3) + b5 )
proof end;

theorem Th69: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 holds
( b3 in b5 iff b4 + b5 = (b4 - b3) + b5 )
proof end;

theorem Th70: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 holds
( b3 in b4 + b5 iff b4 + b5 = b3 + b5 )
proof end;

theorem Th71: :: VECTSP_4:71
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 Subspace of b2 st b3 in b4 + b6 & b3 in b5 + b6 holds
b4 + b6 = b5 + b6
proof end;

theorem Th72: :: VECTSP_4:72
for b1 being Field
for b2 being VectSp of b1
for b3 being Element of b1
for b4 being Element of b2
for b5 being Subspace of b2 st b3 <> 1. b1 & b3 * b4 in b4 + b5 holds
b4 in b5
proof end;

theorem Th73: :: VECTSP_4: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 b1
for b4 being Element of b2
for b5 being Subspace of b2 st b4 in b5 holds
b3 * b4 in b4 + b5
proof end;

theorem Th74: :: VECTSP_4: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 being Element of b2
for b4 being Subspace of b2 st b3 in b4 holds
- b3 in b3 + b4
proof end;

theorem Th75: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 holds
( b3 + b4 in b4 + b5 iff b3 in b5 )
proof end;

theorem Th76: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 holds
( b3 - b4 in b3 + b5 iff b4 in b5 )
proof end;

theorem Th77: :: VECTSP_4:77
canceled;

theorem Th78: :: VECTSP_4:78
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 Subspace of b2 holds
( b3 in b4 + b5 iff ex b6 being Element of b2 st
( b6 in b5 & b3 = b4 - b6 ) )
proof end;

theorem Th79: :: VECTSP_4: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, b4 being Element of b2
for b5 being Subspace of b2 holds
( ex b6 being Element of b2 st
( b3 in b6 + b5 & b4 in b6 + b5 ) iff b3 - b4 in b5 )
proof end;

theorem Th80: :: VECTSP_4: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 Element of b2
for b5 being Subspace of b2 st b3 + b5 = b4 + b5 holds
ex b6 being Element of b2 st
( b6 in b5 & b3 + b6 = b4 )
proof end;

theorem Th81: :: VECTSP_4:81
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 Subspace of b2 st b3 + b5 = b4 + b5 holds
ex b6 being Element of b2 st
( b6 in b5 & b3 - b6 = b4 )
proof end;

theorem Th82: :: VECTSP_4:82
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 strict Subspace of b2 holds
( b3 + b4 = b3 + b5 iff b4 = b5 )
proof end;

theorem Th83: :: VECTSP_4:83
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, b6 being strict Subspace of b2 st b3 + b5 = b4 + b6 holds
b5 = b6
proof end;

theorem Th84: :: VECTSP_4:84
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 Subspace of b2 ex b5 being Coset of b4 st b3 in b5
proof end;

theorem Th85: :: VECTSP_4:85
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 Subspace of b2
for b4 being Coset of b3 holds
( b4 is lineary-closed iff b4 = the carrier of b3 )
proof end;

theorem Th86: :: VECTSP_4:86
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 strict Subspace of b2
for b5 being Coset of b3
for b6 being Coset of b4 st b5 = b6 holds
b3 = b4
proof end;

theorem Th87: :: VECTSP_4:87
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 {b3} is Coset of (0). b2
proof end;

theorem Th88: :: VECTSP_4:88
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 b3 is Coset of (0). b2 holds
ex b4 being Element of b2 st b3 = {b4}
proof end;

theorem Th89: :: VECTSP_4:89
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 Subspace of b2 holds the carrier of b3 is Coset of b3
proof end;

theorem Th90: :: VECTSP_4:90
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 the carrier of b2 is Coset of (Omega). b2
proof end;

theorem Th91: :: VECTSP_4:91
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 b3 is Coset of (Omega). b2 holds
b3 = the carrier of b2
proof end;

theorem Th92: :: VECTSP_4:92
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 Subspace of b2
for b4 being Coset of b3 holds
( 0. b2 in b4 iff b4 = the carrier of b3 )
proof end;

theorem Th93: :: VECTSP_4:93
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 Subspace of b2
for b5 being Coset of b4 holds
( b3 in b5 iff b5 = b3 + b4 )
proof end;

theorem Th94: :: VECTSP_4:94
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 Subspace of b2
for b6 being Coset of b5 st b3 in b6 & b4 in b6 holds
ex b7 being Element of b2 st
( b7 in b5 & b3 + b7 = b4 )
proof end;

theorem Th95: :: VECTSP_4:95
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 Subspace of b2
for b6 being Coset of b5 st b3 in b6 & b4 in b6 holds
ex b7 being Element of b2 st
( b7 in b5 & b3 - b7 = b4 )
proof end;

theorem Th96: :: VECTSP_4:96
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 Subspace of b2 holds
( ex b6 being Coset of b5 st
( b3 in b6 & b4 in b6 ) iff b3 - b4 in b5 )
proof end;

theorem Th97: :: VECTSP_4:97
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 Subspace of b2
for b5, b6 being Coset of b4 st b3 in b5 & b3 in b6 holds
b5 = b6
proof end;

theorem Th98: :: VECTSP_4:98
canceled;

theorem Th99: :: VECTSP_4:99
canceled;

theorem Th100: :: VECTSP_4:100
canceled;

theorem Th101: :: VECTSP_4:101
canceled;

theorem Th102: :: VECTSP_4:102
canceled;

theorem Th103: :: VECTSP_4:103
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative commutative 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 Element of b2 holds (b3 - b4) * b5 = (b3 * b5) - (b4 * b5) by Lemma1;