let n1, n2 be Element of NAT ; :: thesis: 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>; :: thesis: ( 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; :: thesis: verum