Re: [mizar] WELLFND1:1

[trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> Right you are. I was probably annoyed to find a generally useful 
> theorem about functions in an article on well-foundedness, and guessed 
> too quickly that it could also use some generalization. If I bothered 
> to prove it, I'd experience one of the bright sides of verification - 
> proving false things becomes difficult :-).
>
> I'd rather suggest moving the theorem to some article about functions, 
> or changing the comment appropriately and leaving it there until the 
> moving is done.


I have moved it to GRFUNC_1.  (In the proof a theorem  from GRFUNC_1 is 
used. I tried to generalize it, too.
With the same result).

Regards,
Andrzej