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, Th17;
hence <NAT,*,1> = multLoopStr(# NAT,multnat,1 #) by Def31, Th54; :: thesis: verum