set N = <NAT,*,1> ;
( multMagma(# the carrier of <NAT,*,1> ,the multF of <NAT,*,1> #) = <NAT,*> & the_unity_wrt H₂( <NAT,*,1> ) = H₃( <NAT,*,1> ) ) by Def22, Th19;
hence <NAT,*,1> = multLoopStr(# NAT ,multnat ,1 #) by Def31, Th63; :: thesis: verum