set O1 = OwnSymbolsOf S1;
set O2 = OwnSymbolsOf S2;
set f1 = the adicity of S1;
set f2 = the adicity of S2;
set A1 = AtomicFormulaSymbolsOf S1;
set SS1 = AllSymbolsOf S1;
set SS2 = AllSymbolsOf S2;
set z1 = the ZeroF of S1;
set o1 = the OneF of S1;
set z2 = the ZeroF of S2;
set o2 = the OneF of S2;
set E1 = TheEqSymbOf S1;
set E2 = TheEqSymbOf S2;
set N1 = TheNorSymbOf S1;
set N2 = TheNorSymbOf S2;
B0: ( dom the adicity of S1 = (AllSymbolsOf S1) \ { the OneF of S1} & dom the adicity of S2 = (AllSymbolsOf S2) \ { the OneF of S2} ) by FUNCT_2:def 1;
the adicity of S1 c= the adicity of S2 by DefExt0;
then (AllSymbolsOf S1) \ { the OneF of S1} c= (AllSymbolsOf S2) \ { the OneF of S2} by B0, GRFUNC_1:2;
then ((AllSymbolsOf S1) \ {(TheNorSymbOf S1)}) \ {(TheEqSymbOf S1)} c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by XBOOLE_1:33;
then (AllSymbolsOf S1) \ ({(TheNorSymbOf S1)} \/ {(TheEqSymbOf S1)}) c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by XBOOLE_1:41;
then (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by ENUMSET1:1;
then (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ ({(TheNorSymbOf S2)} \/ {(TheEqSymbOf S1)}) by XBOOLE_1:41;
then (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ ({(TheNorSymbOf S2)} \/ {(TheEqSymbOf S2)}) by DefExt0;
then (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ {(TheNorSymbOf S2),(TheEqSymbOf S2)} by ENUMSET1:1;
hence (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) is empty ; :: thesis: verum