take the total PartFunc of X,NAT ; :: thesis: the total PartFunc of X,NAT is total
thus the total PartFunc of X,NAT is total ; :: thesis: verum