Re: I am trying to figure out...

Hi Adem,

On Sat, 24 Oct 2009, Ozyavas, Adem wrote:

> There are two user-defined sets A and B. The first theorem to be proved is:
>
>    for a,A being set st a being Element of A holds a in A;      ::Q1

It holds if (and only if) A is non-empty.

> and the second:
>
>   for f being Function of A,B holds dom f = A;                ::Q2
>
> For Q2 I tried to use
>
> definition
>  let X,Y;
>  let R be Relation of X,Y;
>  attr R is quasi_total means
> :: FUNCT_2:def 1
>
>  X = dom R if Y = {} implies X = {}
>  otherwise R = {};
> end;
>
> and looked into the theorems in FUNCT_2 article. The hypothesis "Y = {} 
> implies X = {}" seems a lot of work and I was wondering if there is 
> another way.

As in the former case, the statement is clearly accepted if Y is 
non-empty. The condition is formulated in this form just to allow 
defining functions from X to Y even in a slightly more general situation.

Best,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================