begin
Lm1:
for c, c1 being complex number holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
begin
Lm2:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
begin
begin
Lm3:
for F being empty FinSequence holds Product F = 1
begin