begin
:: deftheorem Def1 defines vector RLVECT_2:def 1 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th4:
theorem
theorem Th6:
theorem
theorem Th8:
theorem
:: deftheorem RLVECT_2:def 2 :
canceled;
:: deftheorem RLVECT_2:def 3 :
canceled;
:: deftheorem Def4 defines Sum RLVECT_2:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th14:
theorem
theorem
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem
:: deftheorem Def5 defines Linear_Combination RLVECT_2:def 5 :
:: deftheorem defines Carrier RLVECT_2:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def7 defines ZeroLC RLVECT_2:def 7 :
theorem
canceled;
theorem Th30:
:: deftheorem Def8 defines Linear_Combination RLVECT_2:def 8 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th34:
theorem Th35:
:: deftheorem Def9 defines (#) RLVECT_2:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem
theorem Th42:
theorem Th43:
theorem
:: deftheorem Def10 defines Sum RLVECT_2:def 10 :
Lm1:
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th50:
theorem Th51:
theorem
theorem
theorem
:: deftheorem defines = RLVECT_2:def 11 :
:: deftheorem Def12 defines + RLVECT_2:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem Th62:
:: deftheorem Def13 defines * RLVECT_2:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
:: deftheorem defines - RLVECT_2:def 14 :
theorem
canceled;
theorem Th73:
theorem
theorem
theorem
theorem
:: deftheorem defines - RLVECT_2:def 15 :
theorem
canceled;
theorem Th79:
theorem
theorem
theorem Th82:
:: deftheorem Def16 defines LinComb RLVECT_2:def 16 :
:: deftheorem defines @ RLVECT_2:def 17 :
:: deftheorem defines @ RLVECT_2:def 18 :
:: deftheorem Def19 defines LCAdd RLVECT_2:def 19 :
definition
let V be
RealLinearSpace;
func LCMult V -> Function of
[:REAL ,(LinComb V):],
LinComb V means :
Def20:
for
a being
Real for
e being
Element of
LinComb V holds
it . [a,e] = a * (@ e);
existence
ex b1 being Function of [:REAL ,(LinComb V):], LinComb V st
for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
uniqueness
for b1, b2 being Function of [:REAL ,(LinComb V):], LinComb V st ( for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
end;
:: deftheorem Def20 defines LCMult RLVECT_2:def 20 :
:: deftheorem defines LC_RLSpace RLVECT_2:def 21 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th96:
theorem Th97:
theorem Th98:
theorem
:: deftheorem defines LC_RLSpace RLVECT_2:def 22 :