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 for p1, q1, p2, q2 being AllSymbolsOf S -valued FinSequence st p1 in AtomicFormulasOf S & p2 in AtomicFormulasOf S & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 )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 A1:
(
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 A2:
(
p2 = phi2 &
phi2 is
0wff )
;
consider r1 being
relational Element of
S,
T1 being
|.(ar r1).| -element Element of
(AllTermsOf S) * such that A3:
phi1 = <*r1*> ^ ((S -multiCat) . T1)
by A1;
consider r2 being
relational Element of
S,
T2 being
|.(ar r2).| -element Element of
(AllTermsOf S) * such that A4:
phi2 = <*r2*> ^ ((S -multiCat) . T2)
by A2;
assume
p1 ^ q1 = p2 ^ q2
;
( p1 = p2 & q1 = q2 )then A5:
<*r1*> ^ (((S -multiCat) . T1) ^ q1) =
(<*r2*> ^ ((S -multiCat) . T2)) ^ q2
by A1, A2, A3, A4, FINSEQ_1:32
.=
<*r2*> ^ (((S -multiCat) . T2) ^ q2)
by FINSEQ_1:32
;
then A6:
r1 =
(<*r2*> ^ (((S -multiCat) . T2) ^ q2)) . 1
by FINSEQ_1:41
.=
r2
by FINSEQ_1:41
;
set n =
|.(ar r1).|;
set nT =
|.(ar r1).| -tuples_on (AllTermsOf S);
reconsider T11 =
T1,
T22 =
T2 as
Element of
|.(ar r1).| -tuples_on (AllTermsOf S) by FOMODEL0:16, A6;
reconsider P =
(S -multiCat) .: (|.(ar r1).| -tuples_on (AllTermsOf S)) as
AllSymbolsOf S -prefix set ;
A7:
(
(((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;
then A8:
(
(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 A7;
((S -multiCat) . T111) ^ q1 = ((S -multiCat) . T222) ^ q2
by A6, FINSEQ_1:33, A5;
hence
(
p1 = p2 &
q1 = q2 )
by A1, A2, A8, FOMODEL0:def 19, A3, A4, A6;
verum end;
then
AtomicFormulasOf S is AllSymbolsOf S -prefix
;
hence
AtomicFormulasOf S is S -prefix
; verum