let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let X be functional set ; :: thesis:
set EF = ExFormulasOf S;
set L = LettersOf S;
set G1 = R1 S;
let num be Function of NAT,(ExFormulasOf S); :: thesis:
set XX = X addw (D,num);
set f = (D,num) addw X;
set G2 = R2 S;
set G5 = R5 S;
set G8 = R8 S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
assume B0: ( D is isotone & R1 S in D & R2 S in D & R5 S in D & R8 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D -inconsistent ) ; :: thesis:
B1: for nn, mm being Element of NAT st mm in dom ((D,num) addw X) & nn in dom ((D,num) addw X) & nn < mm holds
((D,num) addw X) . nn c= ((D,num) addw X) . mm

let nn, mm be Element of NAT ; :: thesis:
set m = mm;
set n = nn;
assume ( mm in dom ((D,num) addw X) & nn in dom ((D,num) addw X) & nn < mm ) ; :: thesis:
then nn - nn <= mm - nn by XREAL_1:9;
then 0 <= mm - nn ;
then reconsider k = mm - nn as Nat ;
((D,num) addw X) . nn c= ((D,num) addw X) . (nn + k) by Th18, B0;
hence ((D,num) addw X) . nn c= ((D,num) addw X) . mm ; :: thesis:

end;

end;