:: deftheorem Def22 defines TrivialArity FOMODEL1:def 22 :
for S being non degenerated ZeroOneStr
for b₂ being Function of ( the carrier of S \ { the OneF of S}),INT holds
( b₂ = S TrivialArity iff for s being Element of the carrier of S \ { the OneF of S} holds b₂ . s = TrivialArity s );