:: deftheorem Def4 defines GRZ-arity GRZLOG_1:def 8 :
for b₁ being Polish-arity-function of GRZ-symbols holds
( b₁ = GRZ-arity iff for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies b₁ . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b₁ . a = 0 ) ) );