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;
A1:
( 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 Def41;
then
((AllSymbolsOf S1) \ {(TheNorSymbOf S1)}) \ {(TheEqSymbOf S1)} c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)}
by XBOOLE_1:33, GRFUNC_1:2, A1;
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 XBOOLE_1:41;
then
(AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ ({(TheNorSymbOf S2)} \/ {(TheEqSymbOf S2)})
by Def41;
hence
for b1 being set st b1 = (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) holds
b1 is empty
; verum