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