let n, n1 be Nat; :: thesis: [n1,(n1 * n)] in multRel (NAT,n)
( n1 in NAT & n1 * n in NAT ) by ORDINAL1:def 12;
hence [n1,(n1 * n)] in multRel (NAT,n) by Th42; :: thesis: verum