contract UnboundedNaturalMultiply enhances UnboundedNaturalFacility

    procedure Multiply (updates n: Natural, restores m: Natural)
        ensures
            n = #n * m

end UnboundedNaturalMultiply