let n1, n2 be Element of NAT ; for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2
let m1, m2 be Element of <NAT,*,1>; ( n1 = m1 & n2 = m2 implies m1 * m2 = n1 * n2 )
multMagma(# the carrier of <NAT,*,1>, the multF of <NAT,*,1> #) = <NAT,*>
by Def22;
then reconsider x1 = m1, x2 = m2 as Element of <NAT,*> ;
x1 * x2 = m1 * m2
by Th18;
hence
( n1 = m1 & n2 = m2 implies m1 * m2 = n1 * n2 )
by Th50; verum