set f = the adicity of S;
set T = TermSymbolsOf S;
s in TermSymbolsOf S by DefTermal0;
then reconsider nn = ar s as Element of NAT by FUNCT_1:def 7;
not nn is negative ;
hence ( not ar s is negative & ar s is ext-real ) ; :: thesis: verum