set S1 = S;
let S2 be Language-like ; :: thesis: ( S2 is S -extending implies S2 is eligible )
set L1 = LettersOf S;
set L2 = LettersOf S2;
set AS1 = AtomicFormulaSymbolsOf S;
set AS2 = AtomicFormulaSymbolsOf S2;
set a1 = the adicity of S;
set a2 = the adicity of S2;
set E1 = TheEqSymbOf S;
set E2 = TheEqSymbOf S2;
assume Z0: S2 is S -extending ; :: thesis: S2 is eligible
then B0: ( dom the adicity of S = AtomicFormulaSymbolsOf S & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 & TheEqSymbOf S = TheEqSymbOf S2 & the adicity of S c= the adicity of S2 ) by DefExt0, FUNCT_2:def 1;
reconsider a11 = the adicity of S as Subset of the adicity of S2 by Z0, DefExt0;
a11 " {0} c= the adicity of S2 " {0} by RELAT_1:144;
then reconsider L11 = LettersOf S as Subset of (LettersOf S2) ;
not (LettersOf S2) null L11 is finite ;
hence not LettersOf S2 is finite ; :: according to FOMODEL1:def 23 :: thesis: the adicity of S2 . (TheEqSymbOf S2) = - 2
the adicity of S . (TheEqSymbOf S) = - 2 by DefEligible;
then TheEqSymbOf S in dom the adicity of S by FUNCT_1:def 2;
then the adicity of S . (TheEqSymbOf S) = ( the adicity of S2 +* a11) . (TheEqSymbOf S) by FUNCT_4:13
.= the adicity of S2 . (TheEqSymbOf S2) by B0, FUNCT_4:98 ;
hence the adicity of S2 . (TheEqSymbOf S2) = - 2 by DefEligible; :: thesis: verum