let S be Language; AtomicFormulasOf S is S -prefix
set AF = AtomicFormulasOf S;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
set C = S -multiCat ;
now let p1,
q1,
p2,
q2 be
AllSymbolsOf S -valued FinSequence;
( p1 in AtomicFormulasOf S & p2 in AtomicFormulasOf S & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )assume
p1 in AtomicFormulasOf S
;
( p2 in AtomicFormulasOf S & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )then consider phi1 being
string of
S such that C1:
(
p1 = phi1 &
phi1 is
0wff )
;
assume
p2 in AtomicFormulasOf S
;
( p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )then consider phi2 being
string of
S such that C2:
(
p2 = phi2 &
phi2 is
0wff )
;
consider r1 being
relational Element of
S,
T1 being
abs (ar r1) -element Element of
(AllTermsOf S) * such that C3:
phi1 = <*r1*> ^ ((S -multiCat) . T1)
by C1, FOMODEL1:def 35;
consider r2 being
relational Element of
S,
T2 being
abs (ar r2) -element Element of
(AllTermsOf S) * such that C4:
phi2 = <*r2*> ^ ((S -multiCat) . T2)
by C2, FOMODEL1:def 35;
assume
p1 ^ q1 = p2 ^ q2
;
( p1 = p2 & q1 = q2 )then C5:
<*r1*> ^ (((S -multiCat) . T1) ^ q1) =
(<*r2*> ^ ((S -multiCat) . T2)) ^ q2
by C1, C2, C3, C4, FINSEQ_1:32
.=
<*r2*> ^ (((S -multiCat) . T2) ^ q2)
by FINSEQ_1:32
;
then C6:
r1 =
(<*r2*> ^ (((S -multiCat) . T2) ^ q2)) . 1
by FINSEQ_1:41
.=
r2
by FINSEQ_1:41
;
set n =
abs (ar r1);
set nT =
(abs (ar r1)) -tuples_on (AllTermsOf S);
reconsider T11 =
T1,
T22 =
T2 as
Element of
(abs (ar r1)) -tuples_on (AllTermsOf S) by C6, FOMODEL0:16;
reconsider P =
(S -multiCat) .: ((abs (ar r1)) -tuples_on (AllTermsOf S)) as
AllSymbolsOf S -prefix set ;
Z0:
(
(((AllSymbolsOf S) *) \ {{}}) * c= ((AllSymbolsOf S) *) * &
(AllTermsOf S) * c= (((AllSymbolsOf S) *) \ {{}}) * )
;
then
(
T1 in ((AllSymbolsOf S) *) * &
T2 in ((AllSymbolsOf S) *) * &
dom (S -multiCat) = ((AllSymbolsOf S) *) * )
by FUNCT_2:def 1, TARSKI:def 3;
then C8:
(
(S -multiCat) . T11 in P &
(S -multiCat) . T22 in P )
by FUNCT_1:def 6;
reconsider T111 =
T1,
T222 =
T2 as
Element of
((AllSymbolsOf S) *) * by Z0, TARSKI:def 3;
((S -multiCat) . T111) ^ q1 = ((S -multiCat) . T222) ^ q2
by C6, C5, FINSEQ_1:33;
hence
(
p1 = p2 &
q1 = q2 )
by C1, C2, C8, C3, C4, C6, FOMODEL0:def 20;
verum end;
then
AtomicFormulasOf S is AllSymbolsOf S -prefix
by FOMODEL0:def 20;
hence
AtomicFormulasOf S is S -prefix
; verum