let k, m be Nat; :: thesis:
let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let X be functional set ; :: thesis:
set L = LettersOf S;
set F = S -firstChar ;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set EF = ExFormulasOf S;
let num be Function of NAT,(ExFormulasOf S); :: thesis:
set f = (D,num) addw X;
assume B1: ( D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D ) ; :: thesis:
assume B0: ( not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D -inconsistent ) ; :: thesis:
defpred S₁[ Nat] means ( ((D,num) addw X) . k c= ((D,num) addw X) . (k + $1) & not (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . $1) /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not ((D,num) addw X) . $1 is D -inconsistent );
B10: S₁[ 0 ] by B0, DefWit3;
B11: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
reconsider mk = k + m, MM = m + 1, mm = m as Element of NAT by ORDINAL1:def 12;
reconsider phii = num . mm as Element of ExFormulasOf S ;
reconsider phi = num . mm as wff exal string of S by TARSKI:def 3;
reconsider phi1 = head phi as wff string of S ;
reconsider l1 = (S -firstChar) . phi as literal Element of S ;
C2: phi = (<*l1*> ^ phi1) ^ (tail phi) by FOMODEL2:23
.= <*l1*> ^ phi1 ;
reconsider fmk = (D,(num . mk)) AddAsWitnessTo (((D,num) addw X) . mk) as Subset of ((((D,num) addw X) . mk) \/ (AllFormulasOf S)) ;
reconsider fmm = (D,(num . mm)) AddAsWitnessTo (((D,num) addw X) . mm) as Subset of ((((D,num) addw X) . mm) \/ (AllFormulasOf S)) ;
(((D,num) addw X) . mk) \ fmk = {} ;
then ((D,num) addw X) . mk c= fmk by XBOOLE_1:37;
then C0: ( ((D,num) addw X) . mk c= ((D,num) addw X) . (mk + 1) & ((D,num) addw X) . MM = fmm ) by DefWit3;
assume C1: S₁[m] ; :: thesis:
hence ((D,num) addw X) . k c= ((D,num) addw X) . (k + (m + 1)) by C0, XBOOLE_1:1; :: thesis:
(((D,num) addw X) . mm) \ fmm = {} ;
then reconsider fm = ((D,num) addw X) . mm as functional Subset of fmm by XBOOLE_1:37;
reconsider sm = fm /\ (((AllSymbolsOf S) *) \ {{}}) as Subset of (fmm /\ (((AllSymbolsOf S) *) \ {{}})) by XBOOLE_1:26;
reconsider t = fmm \ (((D,num) addw X) . mm) as trivial set ;
reconsider i = (LettersOf S) \ (SymbolsOf sm) as infinite set by C1;
reconsider T = t /\ (((AllSymbolsOf S) *) \ {{}}) as functional finite FinSequence-membered set ;
fmm = fm \/ t by XBOOLE_1:45;
then SymbolsOf (fmm /\ (((AllSymbolsOf S) *) \ {{}})) = SymbolsOf (sm \/ T) by XBOOLE_1:23
.= (SymbolsOf sm) \/ (SymbolsOf T) by FOMODEL0:47 ;
then (LettersOf S) \ (SymbolsOf (fmm /\ (((AllSymbolsOf S) *) \ {{}}))) = i \ (SymbolsOf T) by XBOOLE_1:41;
hence not (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . (m + 1)) /\ (((AllSymbolsOf S) *) \ {{}}))) is finite by DefWit3; :: thesis:
reconsider LF = (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (fm \/ {(head phii)}))) as Subset of (LettersOf S) ;

per cases ;

suppose D0: ( not fm \/ {phii} is D -inconsistent & LF <> {} ) ; :: thesis:

then reconsider LF = LF as non empty Subset of (LettersOf S) ;
set ll2 = the Element of LF;
reconsider l2 = the Element of LF as literal Element of S by TARSKI:def 3;
not the Element of LF in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (fm \/ {(head phii)})) by XBOOLE_0:def 5;
then ( not fm \/ {(<*l1*> ^ phi1)} is D -inconsistent & not l2 is fm \/ {phi1} -occurring ) by D0, C2, FOMODEL2:def 38;
then D1: not fm \/ {((l1,l2) -SymbolSubstIn phi1)} is D -inconsistent by Lm30, B1;
thus not ((D,num) addw X) . (m + 1) is D -inconsistent by D0, DefWit2, D1, C0; :: thesis:

end;

suppose ( fm \/ {phii} is D -inconsistent or not LF <> {} ) ; :: thesis:

hence not ((D,num) addw X) . (m + 1) is D -inconsistent by C1, C0, DefWit2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B10, B11);
hence ( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & not (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not ((D,num) addw X) . m is D -inconsistent ) ; :: thesis: