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