let S be Language; :: thesis: for t being termal string of S holds
( (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t & S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) & S -diagFormula is one-to-one )
let t be termal string of S; :: thesis: ( (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t & S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) & S -diagFormula is one-to-one )
set FF = AllFormulasOf S;
set AF = AtomicFormulasOf S;
set TT = AllTermsOf S;
set AT = AtomicTermsOf S;
set f = S -diagFormula ;
set E = TheEqSymbOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
deffunc H₁( Element of AllTermsOf S) -> Element of ((AllSymbolsOf S) *) \ {{}} = (<*(TheEqSymbOf S)*> ^ $1) ^ $1;
defpred S₁[ set ] means verum;
set IT = { [tt,H₁(tt)] where tt is Element of AllTermsOf S : S₁[tt] } ;
A1: S -diagFormula = { [tt,H₁(tt)] where tt is Element of AllTermsOf S : S₁[tt] } ;
A2: dom (S -diagFormula) = { tt where tt is Element of AllTermsOf S : S₁[tt] } from ALTCAT_2:sch 2(A1);
A3: { tt where tt is Element of AllTermsOf S : S₁[tt] } c= AllTermsOf S from FRAENKEL:sch 10();

now :: thesis: for x being object st x in AllTermsOf S holds
x in dom (S -diagFormula)

let x be object ; :: thesis: ( x in AllTermsOf S implies x in dom (S -diagFormula) )
assume x in AllTermsOf S ; :: thesis: x in dom (S -diagFormula)
then reconsider tt = x as Element of AllTermsOf S ;
[tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] in S -diagFormula ;
hence x in dom (S -diagFormula) by XTUPLE_0:def 12; :: thesis: verum

end;

then A4: AllTermsOf S c= dom (S -diagFormula) by TARSKI:def 3;
then A5: dom (S -diagFormula) = AllTermsOf S by A3, A2, XBOOLE_0:def 10;
A6: for t being termal string of S holds (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t

proof

let t be termal string of S; :: thesis: (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
( [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] in S -diagFormula & tt in dom (S -diagFormula) ) by A5;
hence (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t by FUNCT_1:def 2; :: thesis: verum

end;

hence (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t ; :: thesis: ( S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) & S -diagFormula is one-to-one )

now :: thesis: for x being object st x in AllTermsOf S holds
(S -diagFormula) . x in AtomicFormulasOf S

let x be object ; :: thesis: ( x in AllTermsOf S implies (S -diagFormula) . x in AtomicFormulasOf S )
assume x in AllTermsOf S ; :: thesis: (S -diagFormula) . x in AtomicFormulasOf S
then reconsider tt = x as Element of AllTermsOf S ;
(S -diagFormula) . tt = (<*(TheEqSymbOf S)*> ^ tt) ^ tt by A6;
then reconsider phi0 = (S -diagFormula) . tt as 0wff string of S ;
phi0 in AtomicFormulasOf S ;
hence (S -diagFormula) . x in AtomicFormulasOf S ; :: thesis: verum

end;

hence S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) by A4, A3, A2, XBOOLE_0:def 10, FUNCT_2:3; :: thesis: S -diagFormula is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom (S -diagFormula) & x2 in dom (S -diagFormula) & (S -diagFormula) . x1 = (S -diagFormula) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (S -diagFormula) & x2 in dom (S -diagFormula) & (S -diagFormula) . x1 = (S -diagFormula) . x2 implies x1 = x2 )
assume ( x1 in dom (S -diagFormula) & x2 in dom (S -diagFormula) ) ; :: thesis: ( (S -diagFormula) . x1 = (S -diagFormula) . x2 implies x1 = x2 )
then reconsider tt1 = x1, tt2 = x2 as Element of AllTermsOf S by A3, A2;
( tt1 is Element of ((AllSymbolsOf S) *) \ {{}} & tt2 is Element of ((AllSymbolsOf S) *) \ {{}} ) ;
then reconsider tt11 = tt1, tt22 = tt2 as AllSymbolsOf S -valued non empty FinSequence ;
assume (S -diagFormula) . x1 = (S -diagFormula) . x2 ; :: thesis: x1 = x2
then (S -diagFormula) . tt1 = (<*(TheEqSymbOf S)*> ^ tt2) ^ tt2 by A6;
then (<*(TheEqSymbOf S)*> ^ tt1) ^ tt1 = (<*(TheEqSymbOf S)*> ^ tt2) ^ tt2 by A6
.= <*(TheEqSymbOf S)*> ^ (tt2 ^ tt2) by FINSEQ_1:32 ;
then <*(TheEqSymbOf S)*> ^ (tt1 ^ tt1) = <*(TheEqSymbOf S)*> ^ (tt2 ^ tt2) by FINSEQ_1:32;
then ( tt11 ^ tt11 = tt22 ^ tt22 & tt1 in AllTermsOf S & tt2 in AllTermsOf S ) by FOMODEL0:41;
hence x1 = x2 by FOMODEL0:def 19; :: thesis: verum

end;

hence S -diagFormula is one-to-one by FUNCT_1:def 4; :: thesis: verum