:: deftheorem defines initial-funcs COMPUT_1:def 17 :
initial-funcs = {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;