Re: A question about rng being non empty

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

Piotr Rudnicki wrote:

> Thanks.  But I still have a problem with
>
> > >    consider h being non empty Function of NAT, NAT;
> > > ::>                                  *136
>
> I was under the impression that the conditional cluster from WAYBEL_1
> provides the needed existential cluster.  Am I wrong?
>

No, it only allows for a simple proof of the existential cluster like:

definition
 cluster non empty Function of NAT,NAT;
 existence
  proof consider f being Function of NAT,NAT;
   take f;
   thus thesis;
  end;
end;

The reason is that Mizar does not round up an empty cluster. And reasons for this
seems to be obvious.

Greetings,
Andrzej