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