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 SEQ_4:def 7;
hence a * F = (multcomplex [;] a,(id COMPLEX )) * F by SEQ_4:def 12; :: thesis: verum