set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = |.(ar ((S -firstChar) . t)).|;
A5: (AllSymbolsOf S) -multiCat is |.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
A6: dom ((AllSymbolsOf S) -multiCat) = ((AllSymbolsOf S) *) * by FUNCT_2:def 1;
let IT1, IT2 be Element of (AllTermsOf S) * ; :: thesis: ( IT1 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) & IT2 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) implies IT1 = IT2 )
reconsider IT11 = IT1, IT22 = IT2 as FinSequence of AllTermsOf S by FINSEQ_1:def 11;
assume A7: ( IT1 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) ) ; :: thesis: ( not IT2 is |.(ar ((S -firstChar) . t)).| -element or not t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) or IT1 = IT2 )
then len IT11 = |.(ar ((S -firstChar) . t)).| by CARD_1:def 7;
then reconsider IT111 = IT11 as Element of |.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S) by FINSEQ_2:133;
assume A8: ( IT2 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) ) ; :: thesis: IT1 = IT2
then len IT22 = |.(ar ((S -firstChar) . t)).| by CARD_1:def 7;
then reconsider IT222 = IT22 as Element of |.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S) by FINSEQ_2:133;
A9: ((AllSymbolsOf S) -multiCat) . IT111 = ((AllSymbolsOf S) -multiCat) . IT222 by FINSEQ_1:33, A7, A8;
( IT111 in (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) & IT222 in (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) ) by XBOOLE_0:def 4, A6;
hence IT1 = IT2 by A9, A5; :: thesis: verum