H₁( <NAT,*> ) = NAT by Def31;
hence the_unity_wrt the multF of <NAT,*> = 1 by Th30, BINOP_2:7; :: thesis: verum