let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n holds 1r * z = z
let z be Element of COMPLEX n; :: thesis: 1r * z = z
A1: rng z c= COMPLEX ;
thus 1r * z = (id COMPLEX) * z by BINOP_2:6, FINSEQOP:45
.= z by A1, RELAT_1:79 ; :: thesis: verum