let m, n1, n2 be Nat; :: thesis: ( m const n1 = m const n2 implies n1 = n2 )
set x = the Element of m -tuples_on NAT;
( (m const n1) . the Element of m -tuples_on NAT = n1 & (m const n2) . the Element of m -tuples_on NAT = n2 ) ;
hence ( m const n1 = m const n2 implies n1 = n2 ) ; :: thesis: verum