We define by Definition by recursion on ( fixed):

  1. for limit