Re: A question about rng being non empty

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

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.