let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for T being abs (ar b₂) -element Element of (AllTermsOf S) * holds
( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )
let S be Language; :: thesis: for a being ofAtomicFormula Element of S
for T being abs (ar b₁) -element Element of (AllTermsOf S) * holds
( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )
let a be ofAtomicFormula Element of S; :: thesis: for T being abs (ar a) -element Element of (AllTermsOf S) * holds
( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )
set AT = AllTermsOf S;
set SS = AllSymbolsOf S;
set I = X -freeInterpreter a;
set f = a -compound ;
set m = abs (ar a);
set g = (a -compound) | ((abs (ar a)) -tuples_on (AllTermsOf S));
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
let T be abs (ar a) -element Element of (AllTermsOf S) * ; :: thesis: ( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )
Z2: dom (a -compound) = (((AllSymbolsOf S) *) \ {{}}) * by FUNCT_2:def 1;
T in (abs (ar a)) -tuples_on (AllTermsOf S) by FOMODEL0:16;
then B0: ( ((a -compound) | ((abs (ar a)) -tuples_on (AllTermsOf S))) . T = (a -compound) . T & a -compound T = (a -compound) . T ) by DefCompound1, FUNCT_1:49;
thus ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) by B0, DefFreeInt1; :: thesis: ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) )
assume a is relational ; :: thesis: (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T)
then X -freeInterpreter a = (chi (X,(AtomicFormulasOf S))) * ((a -compound) | ((abs (ar a)) -tuples_on (AllTermsOf S))) by DefFreeInt1
.= ((chi (X,(AtomicFormulasOf S))) * (a -compound)) | ((abs (ar a)) -tuples_on (AllTermsOf S)) by RELAT_1:83 ;
then (X -freeInterpreter a) . T = ((chi (X,(AtomicFormulasOf S))) * (a -compound)) . T by FOMODEL0:16, FUNCT_1:49
.= (chi (X,(AtomicFormulasOf S))) . ((a -compound) . T) by Z2, FUNCT_1:13 ;
hence (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) by DefCompound1; :: thesis: verum