Re: [mizar] Now I know why I cannot quote a theorem as the sawdust remains

[Adam Grabowski <adam@math.uwb.edu.pl>]

On Sat, 29 Nov 2003, Piotr Rudnicki wrote:

> I need both notations from FVSUM1 and from POLYNOM1.  What am I supposed
> to do?
  Maybe slightly off-topic, but aren't the two definenses equivalent?
At least I have just proven their compatibility. Maybe the best solution
is to change the definition from POLYNOM1 into the redefinition and I
think it should be done.
  URN problem remains unsolved, however.
  Adam