set N = TheNorSymbOf S;
set f = the adicity of S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
TheNorSymbOf S in { the ZeroF of S,(TheNorSymbOf S)} by TARSKI:def 2;
then not TheNorSymbOf S in OwnSymbolsOf S by XBOOLE_0:def 5;
hence for b₁ being Element of S st b₁ = TheNorSymbOf S holds
not b₁ is own by DefOwn; :: thesis: verum