theorem Th83: :: COMPUT_1:84

for g being primitive-recursive 2 -ary Function holds (1,2)->(1,?,2) g in PrimRec