let S be Language; :: thesis:
set AF = AtomicFormulasOf S;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
set C = S -multiCat ;
now :: thesis: 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; :: thesis: ( p1 in AtomicFormulasOf S & p2 in AtomicFormulasOf S & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )
assume p1 in AtomicFormulasOf S ; :: thesis: ( 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 ; :: thesis: ( 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 () * such that
A3: phi1 = <*r1*> ^ (() . T1) by A1;
consider r2 being relational Element of S, T2 being |.(ar r2).| -element Element of () * such that
A4: phi2 = <*r2*> ^ (() . T2) by A2;
assume p1 ^ q1 = p2 ^ q2 ; :: thesis: ( p1 = p2 & q1 = q2 )
then A5: <*r1*> ^ ((() . T1) ^ q1) = (<*r2*> ^ (() . T2)) ^ q2 by
.= <*r2*> ^ ((() . T2) ^ q2) by FINSEQ_1:32 ;
then A6: r1 = (<*r2*> ^ ((() . T2) ^ q2)) . 1 by FINSEQ_1:41
.= r2 by FINSEQ_1:41 ;
set n = |.(ar r1).|;
set nT = |.(ar r1).| -tuples_on ();
reconsider T11 = T1, T22 = T2 as Element of |.(ar r1).| -tuples_on () by ;
reconsider P = () .: (|.(ar r1).| -tuples_on ()) as AllSymbolsOf S -prefix set ;
A7: ( (((AllSymbolsOf S) *) \ ) * c= (() *) * & () * c= ((() *) \ ) * ) ;
then ( T1 in (() *) * & T2 in (() *) * & dom () = (() *) * ) by FUNCT_2:def 1;
then A8: ( (S -multiCat) . T11 in P & () . T22 in P ) by FUNCT_1:def 6;
reconsider T111 = T1, T222 = T2 as Element of (() *) * by A7;
((S -multiCat) . T111) ^ q1 = (() . T222) ^ q2 by ;
hence ( p1 = p2 & q1 = q2 ) by ; :: thesis: verum
end;
then AtomicFormulasOf S is AllSymbolsOf S -prefix ;
hence AtomicFormulasOf S is S -prefix ; :: thesis: verum