let S be Language; :: thesis: AllTermsOf S is S -prefix
set SS = AllSymbolsOf S;
set f = (AllSymbolsOf S) -concatenation ;
set F = (AllSymbolsOf S) -multiCat ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;

now

let t1, t2, w1, w2 be set ; :: thesis: ( t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
assume C3: ( t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) ) ; :: thesis: ( t1 = t2 & w1 = w2 )
consider mm being Element of NAT such that
C1: t1 in (S -termsOfMaxDepth) . mm by Lm26, C3;
consider nn being Element of NAT such that
C2: t2 in (S -termsOfMaxDepth) . nn by Lm26, C3;
set p = mm + nn;
C4: (S -termsOfMaxDepth) . (mm + nn) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def 3;
( (S -termsOfMaxDepth) . mm c= (S -termsOfMaxDepth) . (mm + nn) & (S -termsOfMaxDepth) . nn c= (S -termsOfMaxDepth) . (mm + nn) ) by Lm2;
then ( t1 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) ) by C3, C1, C2, XBOOLE_0:def 4;
hence ( t1 = t2 & w1 = w2 ) by C4, FOMODEL0:def 9; :: thesis: verum

end;

then AllTermsOf S is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def 9;
then AllTermsOf S is AllSymbolsOf S -prefix by FOMODEL0:def 3;
hence AllTermsOf S is S -prefix ; :: thesis: verum