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 SEQ_4:def 15
.= (len x) |-> (multcomplex . (cc,0c)) by FINSEQOP:19
.= (len x) |-> (cc * 0c) by BINOP_2:def 5
.= 0c (len x) by SEQ_4:def 15 ;
hence c * (0c (len x)) = 0c (len x) ; :: thesis: verum