for m, n being Element of NAT holds seq (m,n),n are_equipotent