Re: A question about rng being non empty

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

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