[mizar] defining sets recursively

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear All,

Is there a way to define sets recursively in Mizar? I have searched tens of files in the MML and have not seen an example. 
To give an example, I am trying to define the following set:

let S be set which is defined as follows:

(i) real numbers are in S, and
(ii) Assume A1, A2, ..., An are members of S, then <*A1,A2,...,An*> is a member of S. (Here <*...*> is the finite sequence notation from Mizar.)

With recursively defined sets (if possible) I want to define a finite sequence whose range is a subset of S, given below. For example, with the above recursively defined S such a finite sequence in Mizar of range subset of S would be: 
   let fs be FinSequence of S; 

the finite sequence <* 1, 4, <* 3, 12 *>,<*<*7,23*>, 34*>, 22*> is an example of fs as well as <*3,4,1*>. That is every finite sequence of arbitrarily nested finite sequences are examples of fs.

I appreciate your help in advance.

Sincerely,
Adem Ozyavas