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

proof

let c be Element of COMPLEX ; :: thesis: multcomplex . z,c = c
thus multcomplex . z,c = 1 * c by Def5
.= c ; :: thesis: verum

end;

let c be Element of COMPLEX ; :: according to BINOP_1:def 17 :: thesis: multcomplex . c,z = c
thus multcomplex . c,z = c * 1 by Def5
.= c ; :: thesis: verum