let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n holds 0c * z = 0c n
let z be Element of COMPLEX n; :: thesis: 0c * z = 0c n
A1: rng z c= COMPLEX ;
thus 0c * z = multcomplex [;] 0c ,((id COMPLEX ) * z) by FUNCOP_1:44
.= multcomplex [;] 0c ,z by A1, RELAT_1:79
.= 0c n by Th7, Th15, BINOP_2:1, FINSEQOP:80 ; :: thesis: verum