set f = the adicity of S;
reconsider g = the adicity of S as Function of (AtomicFormulaSymbolsOf S),INT ;
reconsider ss = s as Element of AtomicFormulaSymbolsOf S by Def20;
g . ss in INT ;
hence the adicity of S . s is Element of INT ; :: thesis: verum