thus i const j in PrimRec by Th73; :: according to COMPUT_1:def 16 :: thesis: verum