set N = <NAT,+,0> ;
( multMagma(# the carrier of <NAT,+,0>, the multF of <NAT,+,0> #) = <NAT,+> & the_unity_wrt H₂( <NAT,+,0> ) = H₃( <NAT,+,0> ) ) by Def22, Th17;
hence <NAT,+,0> = multLoopStr(# NAT,addnat,0 #) by Th40, Th43; :: thesis: verum