let m be Nat; :: thesis: for S being Language holds (S -termsOfMaxDepth) . m is S -prefix
let S be Language; :: thesis: (S -termsOfMaxDepth) . m is S -prefix
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set L = LettersOf S;
set S1 = 1 -tuples_on (AllSymbolsOf S);
set f = S -cons ;
set F = S -multiCat ;
set ff = (AllSymbolsOf S) -concatenation ;
set FF = (AllSymbolsOf S) -multiCat ;
B10: dom ((AllSymbolsOf S) -multiCat) = ((AllSymbolsOf S) *) * by FUNCT_2:def 1;
reconsider LS = LettersOf S as non empty Subset of (AllSymbolsOf S) ;
set L1 = 1 -tuples_on LS;
defpred S₁[ Nat] means (S -termsOfMaxDepth) . $1 is S -prefix ;
B1: S₁[ 0 ]

proof

(1 -tuples_on LS) /\ (1 -tuples_on (AllSymbolsOf S)) = 1 -tuples_on (LS /\ (AllSymbolsOf S)) by FOMODEL0:3
.= 1 -tuples_on LS by XBOOLE_1:28 ;
then reconsider L11 = 1 -tuples_on LS as Subset of (1 -tuples_on (AllSymbolsOf S)) ;
(S -termsOfMaxDepth) . 0 = AtomicTermsOf S by DefTerm
.= L11 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

B2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume Z5: S₁[m] ; :: thesis: S₁[m + 1]
reconsider mm = m, mm1 = m + 1 as Element of NAT by ORDINAL1:def 12;

now

let t1, t2, w1, w2 be set ; :: thesis: ( t1 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & (S -cons) . (t1,w1) = (S -cons) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
assume Z0: ( t1 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * ) ; :: thesis: ( (S -cons) . (t1,w1) = (S -cons) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
( t1 in (S -termsOfMaxDepth) . mm1 & not t1 in {{}} & t2 in (S -termsOfMaxDepth) . mm1 & not t2 in {{}} ) by Z0;
then reconsider t11 = t1, t22 = t2 as mm + 1 -termal string of S by DefTermal, XBOOLE_0:def 5;
reconsider t111 = t11, t222 = t22 as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
consider T1 being Element of ((S -termsOfMaxDepth) . mm) * such that
C1: ( T1 is abs (ar ((S -firstChar) . t11)) -element & t11 = <*((S -firstChar) . t11)*> ^ ((S -multiCat) . T1) ) by Lm333;
consider T2 being Element of ((S -termsOfMaxDepth) . mm) * such that
C2: ( T2 is abs (ar ((S -firstChar) . t22)) -element & t22 = <*((S -firstChar) . t22)*> ^ ((S -multiCat) . T2) ) by Lm333;
reconsider T11 = T1, T22 = T2 as FinSequence of (S -termsOfMaxDepth) . mm by FINSEQ_1:def 11;
reconsider w11 = w1, w22 = w2 as Element of (AllSymbolsOf S) * by Z0;
reconsider head1 = (S -multiCat) . T1, head2 = (S -multiCat) . T2, tail1 = w11, tail2 = w22 as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
assume (S -cons) . (t1,w1) = (S -cons) . (t2,w2) ; :: thesis: ( t1 = t2 & w1 = w2 )
then t111 ^ w11 = (S -cons) . (t222,w22) by FOMODEL0:4;
then (<*((S -firstChar) . t11)*> ^ ((S -multiCat) . T1)) ^ w11 = t222 ^ w22 by C1, FOMODEL0:4;
then <*((S -firstChar) . t11)*> ^ (((S -multiCat) . T1) ^ w11) = (<*((S -firstChar) . t22)*> ^ ((S -multiCat) . T2)) ^ w22 by C2, FINSEQ_1:32;
then <*((S -firstChar) . t11)*> ^ (head1 ^ tail1) = <*((S -firstChar) . t22)*> ^ (head2 ^ tail2) by FINSEQ_1:32;
then Z1: (S -cons) . (<*((S -firstChar) . t11)*>,(head1 ^ tail1)) = <*((S -firstChar) . t22)*> ^ (head2 ^ tail2) by FOMODEL0:4;
1 -tuples_on (AllSymbolsOf S) c= 1 -tuples_on (AllSymbolsOf S) ;
then reconsider S1 = 1 -tuples_on (AllSymbolsOf S) as Subset of (1 -tuples_on (AllSymbolsOf S)) ;
C4: S1 is S -cons -unambiguous by FOMODEL0:def 3;
S1 /\ ((AllSymbolsOf S) *) = S1 by FINSEQ_2:134, XBOOLE_1:28;
then ( <*((S -firstChar) . t11)*> in S1 /\ ((AllSymbolsOf S) *) & <*((S -firstChar) . t22)*> in S1 /\ ((AllSymbolsOf S) *) & head1 ^ tail1 in (AllSymbolsOf S) * & head2 ^ tail2 in (AllSymbolsOf S) * & (S -cons) . (<*((S -firstChar) . t11)*>,(head1 ^ tail1)) = (S -cons) . (<*((S -firstChar) . t22)*>,(head2 ^ tail2)) ) by Z1, FOMODEL0:4;
then Z3: ( <*((S -firstChar) . t11)*> = <*((S -firstChar) . t22)*> & head1 ^ tail1 = head2 ^ tail2 & head1 ^ tail1 = ((AllSymbolsOf S) -concatenation) . (head1,tail1) ) by C4, FOMODEL0:4, FOMODEL0:def 9;
C6: (S -firstChar) . t11 = (S -firstChar) . t22 by Z3, FINSEQ_1:76;
set n = abs (ar ((S -firstChar) . t11));
( len T11 = abs (ar ((S -firstChar) . t11)) & len T22 = abs (ar ((S -firstChar) . t11)) ) by C1, C6, C2, CARD_1:def 7;
then ( T11 in (abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m) & T22 in (abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m) & T11 in dom ((AllSymbolsOf S) -multiCat) & T22 in dom ((AllSymbolsOf S) -multiCat) ) by B10, FINSEQ_2:133;
then ( ((AllSymbolsOf S) -multiCat) . T11 in ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) & ((AllSymbolsOf S) -multiCat) . T22 in ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) & ((AllSymbolsOf S) -multiCat) . T1 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -multiCat) . T2 in (AllSymbolsOf S) * ) by FUNCT_1:def 6;
then C9: ( ((AllSymbolsOf S) -multiCat) . T1 in (((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m))) /\ ((AllSymbolsOf S) *) & ((AllSymbolsOf S) -multiCat) . T2 in (((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m))) /\ ((AllSymbolsOf S) *) & w11 in (AllSymbolsOf S) * & w22 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . ((((AllSymbolsOf S) -multiCat) . T1),w11) = ((AllSymbolsOf S) -concatenation) . ((((AllSymbolsOf S) -multiCat) . T2),w22) ) by Z3, FOMODEL0:4, XBOOLE_0:def 4;
( (S -termsOfMaxDepth) . m is AllSymbolsOf S -prefix & ( (S -termsOfMaxDepth) . m is AllSymbolsOf S -prefix implies ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) is AllSymbolsOf S -prefix ) ) by Z5, DefSPrefix;
then ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def 3;
hence ( t1 = t2 & w1 = w2 ) by C1, C2, Z3, C9, FOMODEL0:def 9; :: thesis: verum

end;

then (S -termsOfMaxDepth) . (m + 1) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def 9;
then (S -termsOfMaxDepth) . (m + 1) is AllSymbolsOf S -prefix by FOMODEL0:def 3;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(B1, B2);
hence (S -termsOfMaxDepth) . m is S -prefix ; :: thesis: verum