theorem Th17: :: FOMODEL4:17

for k, m being Nat
for S being Language
for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . m is D -consistent )