theorem Th23: :: CATALAN2:23

for n being Nat holds Domin_0 (n,0) = {(n --> 0)}