let x be FinSequence of COMPLEX ; :: thesis: for c being Element of COMPLEX holds c * x = (multcomplex [;] (c,(id COMPLEX))) * x
let c be Element of COMPLEX ; :: thesis: c * x = (multcomplex [;] (c,(id COMPLEX))) * x
c multcomplex = multcomplex [;] (c,(id COMPLEX)) by SEQ_4:def 4;
hence c * x = (multcomplex [;] (c,(id COMPLEX))) * x by SEQ_4:def 9; :: thesis: verum