set f = the adicity of S;
s in LettersOf S by DefLiteral;
then the adicity of S . s in {0} by FUNCT_1:def 7;
hence for b₁ being number st b₁ = ar s holds
b₁ is empty ; :: thesis: verum