begin
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem RLVECT_1:def 1 :
canceled;
:: deftheorem RLVECT_1:def 2 :
canceled;
:: deftheorem RLVECT_1:def 3 :
canceled;
:: deftheorem defines * RLVECT_1:def 4 :
theorem
canceled;
theorem
:: 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 RLVECT_1:def 8 :
canceled;
:: deftheorem Def9 defines RealLinearSpace-like RLVECT_1:def 9 :
:: deftheorem defines Trivial-RLSStruct RLVECT_1:def 10 :
theorem
canceled;
theorem
canceled;
Lm1:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of st v + w = 0. V holds
w + v = 0. V
theorem
canceled;
theorem Th9:
theorem Th10:
:: deftheorem Def11 defines - RLVECT_1:def 11 :
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of ex w being Element of st v + w = u
:: deftheorem defines - RLVECT_1:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem
canceled;
theorem Th33:
theorem
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem
Lm3:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, w being Element of holds - (u + w) = (- w) + (- u)
theorem Th41:
theorem
theorem
theorem Th44:
theorem
theorem
theorem
theorem Th48:
theorem Th49:
theorem
theorem
:: deftheorem Def13 defines Sum RLVECT_1:def 13 :
Lm4:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm5:
for V being non empty addLoopStr
for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th55:
theorem
theorem
theorem Th58:
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of holds Sum <*v*> = v
theorem
theorem
theorem
theorem Th62:
theorem Th63:
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem RLVECT_1:def 14 :
canceled;
:: deftheorem Def15 defines zeroed RLVECT_1:def 15 :
theorem