set f = the adicity of S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
s in LowerCompoundersOf S by DefLowCompounding;
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} by XBOOLE_0:def 5;
hence for b₁ being number st b₁ = ar s holds
not b₁ is empty by TARSKI:def 1; :: thesis: verum