let X be set ; for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let S be Language; for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let r be relational Element of S; for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let D be RuleSet of S; ( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded implies X -freeInterpreter r is (X,D) -termEq -respecting )
assume A1:
( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded )
; X -freeInterpreter r is (X,D) -termEq -respecting
set AT = AllTermsOf S;
set R = (X,D) -termEq ;
set I = X -freeInterpreter r;
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
set SS = AllSymbolsOf S;
set g = r -compound ;
set m = |.(ar r).|;
now for x1, x2 being set st [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) holds
[((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEANlet x1,
x2 be
set ;
( [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) implies [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN )assume A2:
[x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq)
;
[((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEANthen consider T1,
T2 being
|.(ar r).| -element Element of
(AllTermsOf S) * such that A3:
(
T1 = x1 &
T2 = x2 &
PairWiseEq (
T1,
T2)
c= X )
by Lm37, A1;
reconsider w1 =
r -compound T1,
w2 =
r -compound T2 as
0 -wff string of
S ;
(
w1 in AtomicFormulasOf S &
w2 in AtomicFormulasOf S )
;
then reconsider w11 =
w1,
w22 =
w2 as
Element of
AtomicFormulasOf S ;
A4:
(
(r -compound) . x1 = w11 &
(r -compound) . x2 = w22 )
by A3, FOMODEL3:def 2;
(
w11 in X iff
w22 in X )
by A4, A1, A2, Lm40;
then
(
[((chi (X,(AtomicFormulasOf S))) . w1),((chi (X,(AtomicFormulasOf S))) . w2)] in id BOOLEAN &
(X -freeInterpreter r) . T1 = (chi (X,(AtomicFormulasOf S))) . w1 &
(X -freeInterpreter r) . T2 = (chi (X,(AtomicFormulasOf S))) . w2 )
by FOMODEL0:67, FOMODEL3:6;
hence
[((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN
by A3;
verum end;
then
X -freeInterpreter r is |.(ar r).| -placesOf ((X,D) -termEq), id BOOLEAN -respecting
;
hence
X -freeInterpreter r is (X,D) -termEq -respecting
by FOMODEL3:def 10; verum