let x be FinSequence of COMPLEX ; :: thesis: for c being Complex holds c * (0c (len x)) = 0c (len x)
let c be Complex; :: 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:34
.= multcomplex [;] (cc,(0c (len x))) by A1, RELAT_1:53
.= multcomplex [;] (cc,((len x) |-> 0c)) by SEQ_4:def 12
.= (len x) |-> (multcomplex . (cc,0c)) by FINSEQOP:18
.= (len x) |-> (cc * 0c) by BINOP_2:def 5
.= 0c (len x) by SEQ_4:def 12 ;
hence c * (0c (len x)) = 0c (len x) ; :: thesis: verum