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

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