thus for c being Element of COMPLEX holds addcomplex . z,c = c :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: z is_a_right_unity_wrt addcomplex

proof

let c be Element of COMPLEX ; :: thesis: addcomplex . z,c = c
thus addcomplex . z,c = 0 + c by Def3
.= c ; :: thesis: verum

end;

let c be Element of COMPLEX ; :: according to BINOP_1:def 17 :: thesis: addcomplex . c,z = c
thus addcomplex . c,z = c + 0 by Def3
.= c ; :: thesis: verum