let x be FinSequence of COMPLEX ; :: thesis: for c being complex number holds c * (0c (len x)) = 0c (len x)
let c be complex number ; :: thesis: c * (0c (len x)) = 0c (len x)
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
A1: rng (0c (len x)) c= COMPLEX by FINSEQ_1:def 4;
c * (0c (len x)) = (multcomplex [;] cc,(id COMPLEX )) * (0c (len x)) by Lm1
.= multcomplex [;] cc,((id COMPLEX ) * (0c (len x))) by FUNCOP_1:44
.= multcomplex [;] cc,(0c (len x)) by A1, RELAT_1:79
.= multcomplex [;] cc,((len x) |-> 0c ) by COMPLSP1:def 13
.= (len x) |-> (multcomplex . cc,0c ) by FINSEQOP:19
.= (len x) |-> (cc * 0c ) by BINOP_2:def 5
.= 0c (len x) by COMPLSP1:def 13 ;
hence c * (0c (len x)) = 0c (len x) ; :: thesis: verum