Hello All, I wrote a recursive function in Mizar which takes two arguments, two natural numbers, and maps them to another natural number. I searched the MML and could not find a scheme that I could use in the proof of correctness (existence and uniqueness) of that function. I appreciate any help. Adem Ozyavas