I am trying to figure out...

Hello All,

I would like to thank for your very helpful comments and time.. 
 I have tried and still trying to figrue out the answers to 2 questions formulated below. 

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

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.

Thank you again very much and have a nice weekend.

Adem Ozyavas