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