let n be 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:44
.= z by A1, RELAT_1:53 ; :: thesis: verum