set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = abs (ar ((S -firstChar) . t));
C11: (AllSymbolsOf S) -multiCat is (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
C0: dom ((AllSymbolsOf S) -multiCat) = ((AllSymbolsOf S) *) * by FUNCT_2:def 1;
let IT1, IT2 be Element of (AllTermsOf S) * ; :: thesis: ( IT1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) & IT2 is abs (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 C1: ( IT1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) ) ; :: thesis: ( not IT2 is abs (ar ((S -firstChar) . t)) -element or not t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) or IT1 = IT2 )
then len IT11 = abs (ar ((S -firstChar) . t)) by CARD_1:def 7;
then reconsider IT111 = IT11 as Element of (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) by FINSEQ_2:133;
assume C2: ( IT2 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) ) ; :: thesis: IT1 = IT2
then len IT22 = abs (ar ((S -firstChar) . t)) by CARD_1:def 7;
then reconsider IT222 = IT22 as Element of (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) by FINSEQ_2:133;
C3: ((AllSymbolsOf S) -multiCat) . IT111 = ((AllSymbolsOf S) -multiCat) . IT222 by C1, C2, FINSEQ_1:33;
( IT111 in ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) & IT222 in ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) ) by C0, XBOOLE_0:def 4;
hence IT1 = IT2 by C3, C11, FOMODEL0:def 5; :: thesis: verum