theorem :: SEQ_4:53

1r is_a_unity_wrt multcomplex by BINOP_2:6, SETWISEO:14;