let a be Element of COMPLEX ; :: thesis: for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] a,(id COMPLEX )) * F
let F be FinSequence of COMPLEX ; :: thesis: a * F = (multcomplex [;] a,(id COMPLEX )) * F
a multcomplex = multcomplex [;] a,(id COMPLEX ) by COMPLSP1:def 5;
hence a * F = (multcomplex [;] a,(id COMPLEX )) * F by COMPLSP1:def 10; :: thesis: verum