let i be Nat; :: thesis: for R being i -long FinSequence of COMPLEX holds 0c * R = i |-> 0c
let R be i -long FinSequence of COMPLEX ; :: thesis: 0c * R = i |-> 0c
A1: rng R c= COMPLEX ;
thus 0c * R = multcomplex [;] (0c,((id COMPLEX) * R)) by FUNCOP_1:44
.= multcomplex [;] (0c,R) by A1, RELAT_1:79
.= i |-> 0c by SEQ_4:71, SEQ_4:68, BINOP_2:1, FINSEQOP:80 ; :: thesis: verum