let S be Language; :: thesis:
set o = the OneF of S;
set z = the ZeroF of S;
set f = the adicity of S;
set R = RelSymbolsOf S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
set e = TheEqSymbOf S;
set n = TheNorSymbOf S;
set A = AtomicFormulaSymbolsOf S;
set D = the carrier of S \ { the OneF of S};
set L = LowerCompoundersOf S;
set T = TermSymbolsOf S;
set OP = OpSymbolsOf S;
set B = LettersOf S;
thus (LettersOf S) /\ (OpSymbolsOf S) = the adicity of S " ({0} /\ (NAT \ {0})) by FUNCT_1:68
.= the adicity of S " {} by XBOOLE_1:79, XBOOLE_0:def 7
.= {} ; :: thesis:
thus (TermSymbolsOf S) /\ (LowerCompoundersOf S) = the adicity of S " (NAT /\ (INT \ {0})) by FUNCT_1:68
.= the adicity of S " ((NAT /\ INT) \ {0}) by XBOOLE_1:49
.= OpSymbolsOf S by XBOOLE_1:28, XBOOLE_1:7 ; :: thesis:
A1: TheEqSymbOf S in RelSymbolsOf S by Def17;
OwnSymbolsOf S = ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} by XBOOLE_1:41;
then (RelSymbolsOf S) \ (OwnSymbolsOf S) = ((RelSymbolsOf S) \ ( the carrier of S \ { the OneF of S})) \/ ((RelSymbolsOf S) /\ { the ZeroF of S}) by XBOOLE_1:52
.= {} \/ ((RelSymbolsOf S) /\ { the ZeroF of S})
.= { the ZeroF of S} by ZFMISC_1:46, A1 ;
hence (RelSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} ; :: thesis:
thus OwnSymbolsOf S c= AtomicFormulaSymbolsOf S by XBOOLE_1:34, ZFMISC_1:7; :: thesis:
( the adicity of S " {0} c= the adicity of S " NAT & RelSymbolsOf S = ( the adicity of S " INT) \ ( the adicity of S " NAT) & LowerCompoundersOf S = ( the adicity of S " INT) \ ( the adicity of S " {0}) ) by FUNCT_1:69, RELAT_1:143;
hence RelSymbolsOf S c= LowerCompoundersOf S by XBOOLE_1:34; :: thesis:
OpSymbolsOf S = ( the adicity of S " NAT) \ ( the adicity of S " {0}) by FUNCT_1:69;
hence OpSymbolsOf S c= TermSymbolsOf S ; :: thesis:
thus LettersOf S c= TermSymbolsOf S by RELAT_1:143; :: thesis:
- 2 = the adicity of S . (TheEqSymbOf S) by Def23
.= the adicity of S . the ZeroF of S ;
then not the adicity of S . the ZeroF of S in NAT ;
then not the ZeroF of S in the adicity of S " NAT by FUNCT_1:def 7;
then ( the adicity of S " NAT misses { the ZeroF of S} & the adicity of S " NAT c= the carrier of S \ { the OneF of S} ) by ZFMISC_1:50;
then the adicity of S " NAT c= ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} by XBOOLE_1:86;
hence TermSymbolsOf S c= OwnSymbolsOf S by XBOOLE_1:41; :: thesis:
for x being object st x in NAT holds
x in INT by INT_1:def 2;
then NAT \ {0} c= INT \ {0} by XBOOLE_1:33, TARSKI:def 3;
hence OpSymbolsOf S c= LowerCompoundersOf S by RELAT_1:143; :: thesis:
thus LowerCompoundersOf S c= AtomicFormulaSymbolsOf S ; :: thesis: