begin
:: deftheorem VECTSP_6:def 1 :
canceled;
:: deftheorem VECTSP_6:def 2 :
canceled;
:: deftheorem VECTSP_6:def 3 :
canceled;
:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
:: deftheorem defines Carrier VECTSP_6:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :
theorem
canceled;
theorem Th22:
:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def8 defines (#) VECTSP_6:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
theorem Th37:
:: deftheorem Def9 defines Sum VECTSP_6:def 9 :
Lm1:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF holds Sum (ZeroLC V) = 0. V
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem
theorem
:: deftheorem defines = VECTSP_6:def 10 :
:: deftheorem Def11 defines + VECTSP_6:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem
:: deftheorem Def12 defines * VECTSP_6:def 12 :
theorem
canceled;
theorem
canceled;
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
theorem Th64:
theorem
:: deftheorem defines - VECTSP_6:def 13 :
Lm2:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a
theorem
canceled;
theorem Th67:
theorem
Lm3:
for GF being Field holds - (1. GF) <> 0. GF
theorem Th69:
theorem
:: deftheorem defines - VECTSP_6:def 14 :
theorem
canceled;
theorem
canceled;
theorem Th73:
theorem
theorem
theorem Th76:
theorem Th77:
theorem
theorem Th79:
theorem
theorem
theorem