Lm1:
for r, r1 being Real holds (multreal [;] (r,(id REAL))) . r1 = r * r1
Lm2:
for F being real-valued FinSequence holds F is FinSequence of REAL
Lm3:
for F being empty FinSequence holds Product F = 1
Lm4:
for p being complex-valued FinSequence st len p <> 0 holds
ex q being complex-valued FinSequence ex d being Complex st p = q ^ <*d*>
Lm5:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
theorem
for
r1,
r2,
r3,
r4 being
Real holds
Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4