theorem :: SEQ_4:49

0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:14;