:: deftheorem Def21 defines TrivialArity FOMODEL1:def 21 :
for S being ZeroOneStr
for s being Element of the carrier of S \ { the OneF of S} holds
( ( s = the ZeroF of S implies TrivialArity s = - 2 ) & ( not s = the ZeroF of S implies TrivialArity s = 0 ) );