begin
:: deftheorem Def2 defines sqrcomplex RVSUM_2:def 1 :
theorem
Lm3:
for c, c1 being complex number holds (multcomplex [;] c,(id COMPLEX )) . c1 = c * c1
theorem
begin
Lm4:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
:: deftheorem defines + RVSUM_2:def 2 :
theorem
theorem
theorem
theorem
:: deftheorem defines - RVSUM_2:def 3 :
theorem
theorem Th39:
theorem
theorem Th45:
:: deftheorem defines - RVSUM_2:def 4 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines * RVSUM_2:def 5 :
theorem
theorem Th70:
theorem
theorem
:: deftheorem defines mlt RVSUM_2:def 6 :
theorem
theorem
theorem Th92:
theorem
begin
theorem Th102:
theorem
theorem Th104:
theorem Th105:
theorem
theorem Th107:
theorem
theorem Th110:
theorem
theorem
theorem Th118:
theorem Th119:
theorem
begin
Lm5:
for F being empty FinSequence holds Product F = 1
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th137:
theorem
begin
theorem
theorem
theorem
theorem
theorem