let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let S be Language; :: thesis: for D being RuleSet of S
for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let s be low-compounding Element of S; :: thesis: ( {(R#3d S)} c= D & X is D -expanded & s is termal implies X -freeInterpreter s is (X,D) -termEq -respecting )
set n = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set R = (X,D) -termEq ;
set I = X -freeInterpreter s;
assume A1: {(R#3d S)} c= D ; :: thesis: ( not X is D -expanded or not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume A2: X is D -expanded ; :: thesis: ( not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume s is termal ; :: thesis: X -freeInterpreter s is (X,D) -termEq -respecting
then reconsider ss = s as termal Element of S ;
A3: not ss is relational ;

now :: thesis: for x1, x2 being set st [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) holds
[((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq

let x1, x2 be set ; :: thesis: ( [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) implies [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq )
assume [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) ; :: thesis: [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq
then consider T1, T2 being |.(ar s).| -element Element of (AllTermsOf S) * such that
A4: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm37, A2;
set Z = PairWiseEq (T1,T2);
reconsider t1 = ss -compound T1, t2 = ss -compound T2 as termal string of S ;
reconsider ZZ = PairWiseEq (T1,T2) as Subset of X by A4;
{[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is {} ,{(R#3d S)} -derivable by Lm35;
then A5: {[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is {} ,D -derivable by A1, Lm18;
A6: (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is ZZ,D -provable by A5;
( (X -freeInterpreter s) . T1 = t1 & (X -freeInterpreter s) . T2 = t2 ) by FOMODEL3:6;
hence [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq by A6, A4; :: thesis: verum

end;

then X -freeInterpreter s is |.(ar s).| -placesOf ((X,D) -termEq),(X,D) -termEq -respecting ;
hence X -freeInterpreter s is (X,D) -termEq -respecting by FOMODEL3:def 10, A3; :: thesis: verum