Re: There exist duplicated theorems in Mizar

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

Chen Jingchao wrote:

> Recently I found  Theorem FUNCT_4:42 and FUNCT_4:45 are
> completely identical, both of which are described as follows
>     not x in dom g implies (f +.g).x = f.x.
> The article containing the two theorems was finished by 1990.
> Why are not the duplicated thorems still deleted  untill now ?

It is a result of a revision. If I recall originally it was:

   x in dom f & not x in dom g implies (f+.g).x = f.x

   x in dom f \ dom g implies (f+.g).x = f.x

When permissiveness of FUNCT_1:def 4 had been broken, then the
assumption x in dom f ceased to be necessary:

If x is neither in dom f nor in dom g, then it is not in dom(f+.g). So
   (f+.g).x = {}, and f.x = {}, too.

But you of course right. One of them must be removed, Artur Kornilowicz
works on implementing a suitable software.

Regards,
Andrzej Trybulec