let X be set ; :: thesis: for S being Language

for a being ofAtomicFormula Element of S

for T being |.(ar b_{2}).| -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_{1}).| -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

for a being ofAtomicFormula Element of S

for T being |.(ar b

( ( 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

( ( 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