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