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