set f = the adicity of S;
s in LettersOf S by Def14;
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 zero ; :: thesis: verum