let n be 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:34
.= multcomplex [;] (0c,z) by A1, RELAT_1:53
.= 0c n by Th51, Th54, BINOP_2:1, FINSEQOP:76 ; :: thesis: verum