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

proof

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

end;

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