set f = the adicity of S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
s in LowerCompoundersOf S by Def15;
then ( s in dom the adicity of S & the adicity of S . s in INT \ {0} ) by FUNCT_1:def 7;
then not the adicity of S . s in {0} ;
hence for b₁ being number st b₁ = ar s holds
not b₁ is zero by TARSKI:def 1; :: thesis: verum