set f = the adicity of S;
set T = TermSymbolsOf S;
s in TermSymbolsOf S by Def18;
then reconsider nn = ar s as Element of NAT by FUNCT_1:def 7;
not nn is negative ;
hence for b₁ being ExtReal st b₁ = ar s holds
not b₁ is negative ; :: thesis: verum