let i be Nat; :: thesis: for R being i -element complex-valued FinSequence holds 0c * R = i |-> 0c
let R be i -element complex-valued FinSequence; :: thesis: 0c * R = i |-> 0c
A1: rng R c= COMPLEX ;
A2: R is i -element FinSequence of COMPLEX by FINSEQ_1:102;
thus 0c * R = multcomplex [;] (0c,((id COMPLEX) * R)) by FUNCOP_1:34
.= multcomplex [;] (0c,R) by A1, RELAT_1:53
.= i |-> 0c by A2, BINOP_2:1, FINSEQOP:76, SEQ_4:51, SEQ_4:54 ; :: thesis: verum