begin
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines diffreal RVSUM_1:def 1 :
:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem
:: deftheorem defines multreal RVSUM_1:def 3 :
Lm3:
for r, r1 being real number holds (multreal [;] r,(id REAL )) . r1 = r * r1
theorem
canceled;
theorem
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem
Lm4:
for F being real-valued FinSequence holds F is FinSequence of REAL
:: deftheorem defines + RVSUM_1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
:: deftheorem defines - RVSUM_1:def 5 :
theorem
theorem
theorem
theorem Th39:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th45:
:: deftheorem defines - RVSUM_1:def 6 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
:: deftheorem defines * RVSUM_1:def 7 :
theorem
theorem
theorem
theorem Th70:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines sqr RVSUM_1:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th83:
theorem Th84:
:: deftheorem defines mlt RVSUM_1:def 9 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th92:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th98:
theorem Th99:
theorem
:: deftheorem RVSUM_1:def 10 :
canceled;
:: deftheorem Def11 defines Sum RVSUM_1:def 11 :
theorem Th101:
:: deftheorem defines Sum RVSUM_1:def 12 :
:: deftheorem defines Sum RVSUM_1:def 13 :
theorem Th102:
theorem
theorem Th104:
theorem Th105:
theorem
theorem Th107:
theorem Th108:
theorem
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
theorem Th114:
theorem Th115:
theorem Th116:
theorem Th117:
theorem Th118:
theorem Th119:
theorem Th120:
theorem
theorem
:: deftheorem Def14 defines Product RVSUM_1:def 14 :
theorem Th123:
:: deftheorem defines Product RVSUM_1:def 15 :
:: deftheorem defines Product RVSUM_1:def 16 :
Lm5:
for F being empty FinSequence holds Product F = 1
theorem Th124:
theorem Th125:
theorem Th126:
theorem Th127:
theorem
theorem Th129:
theorem
theorem
theorem
Lm6:
for p being complex-valued FinSequence st len p <> 0 holds
ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*>
theorem
theorem
theorem
theorem
theorem Th137:
theorem
theorem
begin
theorem
theorem
theorem
theorem
begin
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
:: deftheorem defines |( RVSUM_1:def 17 :
theorem Th11:
theorem Th19:
theorem Th20:
theorem Th22:
theorem
theorem Th25:
theorem
theorem Th29:
theorem Th30:
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th43:
theorem
theorem Th46:
theorem
theorem Th50:
theorem Th51:
theorem
theorem Th53:
theorem
:: deftheorem Def3 defines are_orthogonal RVSUM_1:def 18 :
theorem
theorem