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 :: thesis: for t1, t2, w1, w2 being set st 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) holds
( t1 = t2 & w1 = w2 )

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 A1: ( 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
A2: t1 in (S -termsOfMaxDepth) . mm by Lm6, A1;
consider nn being Element of NAT such that
A3: t2 in (S -termsOfMaxDepth) . nn by Lm6, A1;
set p = mm + nn;
A4: (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 Lm5;
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 A1, XBOOLE_0:def 4, A2, A3;
hence ( t1 = t2 & w1 = w2 ) by A4; :: thesis: verum

end;

then AllTermsOf S is AllSymbolsOf S -prefix by FOMODEL0:def 10;
hence AllTermsOf S is S -prefix ; :: thesis: verum