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