Re: A question about rng being non empty

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hi,

due to cluster in WAYBEL_1 you do not have to write "non empty Function of
NAT,NAT". "Function of NAT,NAT" is enough.

Artur

On Thu, 7 Jun 2001, 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?
>
> PR
>
>
> On Thu, Jun 07, 2001 at 09:10:01AM +0200, Artur Kornilowicz wrote:
> >
> > The following clusters should be useful:
> >
> > definition  :: YELLOW_6
> >  cluster non empty constant Function;
> > end;
> >
> > definition let A,B be non empty set;  :: WAYBEL_1
> >  cluster -> non empty Function of A,B;
> > end;
> >
> > definition    :: INDEX_1
> >  let f be non empty Function;
> >  cluster rng f -> non empty;
> > end;
> >
> > Greetings
> >
> > Artur Kornilowicz
> >
> > > Hi:
> > >
> > > I must be getting rusty, no matter what I do I cannot get rid of these errors:
> > >
> > >    consider g being non empty Function;
> > > ::>                                  *136
> > >    consider h being non empty Function of NAT, NAT;
> > > ::>                                  *136
> > >    consider f being Function of NAT,NAT;
> > >    rng f is non empty;
> > > ::>                 *4
>
> --
> Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
> email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr
>
> I am a fundamentalist: always fun before mental.
>