set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set n = |.(ar ((S -firstChar) . phi)).|;
A3: ( dom (S -multiCat) = ((AllSymbolsOf S) *) * & (AllTermsOf S) * c= ((AllSymbolsOf S) *) * ) by FUNCT_2:def 1;
reconsider s = (S -firstChar) . phi as Element of AllSymbolsOf S ;
reconsider head = <*s*> as FinSequence of AllSymbolsOf S ;
let IT1, IT2 be |.(ar ((S -firstChar) . phi)).| -element Element of (AllTermsOf S) * ; :: thesis: ( phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT1) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT2) implies IT1 = IT2 )
reconsider I1 = IT1, I2 = IT2 as FinSequence of AllTermsOf S by FINSEQ_1:def 11;
( len IT1 = |.(ar ((S -firstChar) . phi)).| & len IT2 = |.(ar ((S -firstChar) . phi)).| ) by CARD_1:def 7;
then reconsider I11 = I1, I22 = I2 as Element of |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) by FINSEQ_2:133;
reconsider tail1 = (S -multiCat) . IT1, tail2 = (S -multiCat) . IT2 as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
assume A4: ( phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT1) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT2) ) ; :: thesis: IT1 = IT2
( IT1 in dom (S -multiCat) & I11 in |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) & IT2 in dom (S -multiCat) & I22 in |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) ) by A3;
then A5: ( IT1 in (|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & IT2 in (|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & (S -multiCat) . IT1 = (S -multiCat) . IT2 ) by A4, FINSEQ_1:33, XBOOLE_0:def 4;
S -multiCat is |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
hence IT1 = IT2 by A5; :: thesis: verum