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