let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for T being |.(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 |.(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 |.(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 = |.(ar a).|;
set g = (a -compound) | (|.(ar a).| -tuples_on (AllTermsOf S));
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
let T be |.(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) ) )
A1: dom (a -compound) = (((AllSymbolsOf S) *) \ {{}}) * by FUNCT_2:def 1;
A2: ( ((a -compound) | (|.(ar a).| -tuples_on (AllTermsOf S))) . T = (a -compound) . T & a -compound T = (a -compound) . T ) by FOMODEL0:16, FUNCT_1:49, Def2;
thus ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) by A2, Def3; :: 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) | (|.(ar a).| -tuples_on (AllTermsOf S))) by Def3
.= ((chi (X,(AtomicFormulasOf S))) * (a -compound)) | (|.(ar a).| -tuples_on (AllTermsOf S)) by RELAT_1:83 ;
then (X -freeInterpreter a) . T = ((chi (X,(AtomicFormulasOf S))) * (a -compound)) . T by FUNCT_1:49, FOMODEL0:16
.= (chi (X,(AtomicFormulasOf S))) . ((a -compound) . T) by FUNCT_1:13, A1 ;
hence (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) by Def2; :: thesis: verum