begin
:: deftheorem Def2 defines sqrcomplex RVSUM_2:def 1 :
for b1 being UnOp of COMPLEX holds
( b1 = sqrcomplex iff for c being complex number holds b1 . c = c ^2 );
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 :
for F1, F2 being complex-valued FinSequence holds F1 + F2 = addcomplex .: F1,F2;
theorem
theorem
theorem
theorem
:: deftheorem defines - RVSUM_2:def 3 :
for F being complex-valued FinSequence holds - F = compcomplex * F;
theorem
theorem Th39:
theorem
theorem Th45:
:: deftheorem defines - RVSUM_2:def 4 :
for F1, F2 being complex-valued FinSequence holds F1 - F2 = diffcomplex .: F1,F2;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines * RVSUM_2:def 5 :
for F being complex-valued FinSequence
for c being complex number holds c * F = (c multcomplex ) * F;
theorem
theorem Th70:
theorem
theorem
:: deftheorem defines mlt RVSUM_2:def 6 :
for F1, F2 being complex-valued FinSequence holds mlt F1,F2 = multcomplex .: F1,F2;
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