set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set n = abs (ar ((S -firstChar) . phi));
Z1: ( 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 abs (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 = abs (ar ((S -firstChar) . phi)) & len IT2 = abs (ar ((S -firstChar) . phi)) ) by CARD_1:def 7;
then reconsider I11 = I1, I22 = I2 as Element of (abs (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 Z2: ( phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT1) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT2) ) ; :: thesis: IT1 = IT2
( IT1 in dom (S -multiCat) & I11 in (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) & IT2 in dom (S -multiCat) & I22 in (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) ) by Z1;
then B3: ( IT1 in ((abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & IT2 in ((abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & (S -multiCat) . IT1 = (S -multiCat) . IT2 ) by Z2, FINSEQ_1:33, XBOOLE_0:def 4;
S -multiCat is (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
hence IT1 = IT2 by B3, FOMODEL0:def 5; :: thesis: verum