let D be non empty set ; :: thesis: Lang (TotalGrammar D) = D *
set T = TotalGrammar D;
set I = <*the InitialSym of (TotalGrammar D)*>;
defpred S₁[ Element of NAT ] means for p being String of (TotalGrammar D) st len p = $1 & p in D * holds
p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*>;
A1: D c= succ D by XBOOLE_1:7;
A2: the Rules of (TotalGrammar D) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{} ]} by Def10;
A3: the InitialSym of (TotalGrammar D) = D by Def10;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: for p being String of (TotalGrammar D) st len p = k & p in D * holds
p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> ; :: thesis: S₁[k + 1]
let p be String of (TotalGrammar D); :: thesis: ( len p = k + 1 & p in D * implies p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> )
assume that
A6: len p = k + 1 and
A7: p in D * ; :: thesis: p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*>
consider q being FinSequence, a being set such that
A8: p = q ^ <*a*> and
A9: len q = k by A6, TREES_2:4;
A10: rng <*a*> = {a} by FINSEQ_1:55;
<*a*> is FinSequence of the carrier of (TotalGrammar D) by A8, FINSEQ_1:50;
then A11: {a} c= the carrier of (TotalGrammar D) by A10, FINSEQ_1:def 4;
A12: q is FinSequence of the carrier of (TotalGrammar D) by A8, FINSEQ_1:50;
A13: p is FinSequence of D by A7, FINSEQ_1:def 11;
then A14: q is FinSequence of D by A8, FINSEQ_1:50;
<*a*> is FinSequence of D by A8, A13, FINSEQ_1:50;
then A15: {a} c= D by A10, FINSEQ_1:def 4;
reconsider q = q as String of (TotalGrammar D) by A12, FINSEQ_1:def 11;
reconsider a = a as Element of D by A15, ZFMISC_1:37;
reconsider x = a as Symbol of (TotalGrammar D) by A11, ZFMISC_1:37;
[D,<*a,D*>] in { [D,<*d,D*>] where d is Element of D : d = d } ;
then [D,<*a,D*>] in the Rules of (TotalGrammar D) by A2, XBOOLE_0:def 3;
then the InitialSym of (TotalGrammar D) ==> <*x,the InitialSym of (TotalGrammar D)*> by A3, Def1;
then <*the InitialSym of (TotalGrammar D)*> ==> <*x,the InitialSym of (TotalGrammar D)*> by Th3;
then A16: q ^ <*the InitialSym of (TotalGrammar D)*> ==> q ^ <*x,the InitialSym of (TotalGrammar D)*> by Th5;
<*x,the InitialSym of (TotalGrammar D)*> = <*x*> ^ <*the InitialSym of (TotalGrammar D)*> by FINSEQ_1:def 9;
then q ^ <*the InitialSym of (TotalGrammar D)*> ==> p ^ <*the InitialSym of (TotalGrammar D)*> by A8, A16, FINSEQ_1:45;
then A17: p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from q ^ <*the InitialSym of (TotalGrammar D)*> by Th7;
q in D * by A14, FINSEQ_1:def 11;
then q ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> by A5, A9;
hence p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> by A17, Th8; :: thesis: verum

end;

[D,{} ] in {[D,{} ]} by TARSKI:def 1;
then [D,{} ] in the Rules of (TotalGrammar D) by A2, XBOOLE_0:def 3;
then the InitialSym of (TotalGrammar D) ==> <*> the carrier of (TotalGrammar D) by A3, Def1;
then A18: <*the InitialSym of (TotalGrammar D)*> ==> <*> the carrier of (TotalGrammar D) by Th3;
A19: Terminals (TotalGrammar D) = D by Th16;
thus Lang (TotalGrammar D) c= D * :: according to XBOOLE_0:def 10 :: thesis: D * c= Lang (TotalGrammar D)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Lang (TotalGrammar D) or a in D * )
assume a in Lang (TotalGrammar D) ; :: thesis: a in D *
then consider p being String of (TotalGrammar D) such that
A20: a = p and
A21: rng p c= Terminals (TotalGrammar D) and
p is_derivable_from <*the InitialSym of (TotalGrammar D)*> ;
p is FinSequence of D by A19, A21, FINSEQ_1:def 4;
hence a in D * by A20, FINSEQ_1:def 11; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in D * or a in Lang (TotalGrammar D) )
assume A22: a in D * ; :: thesis: a in Lang (TotalGrammar D)
then reconsider a = a as FinSequence of D by FINSEQ_1:def 11;
the carrier of (TotalGrammar D) = succ D by Def10;
then rng a c= the carrier of (TotalGrammar D) by A1, XBOOLE_1:1;
then a is FinSequence of the carrier of (TotalGrammar D) by FINSEQ_1:def 4;
then reconsider n = a as String of (TotalGrammar D) by FINSEQ_1:def 11;
n ^ {} = n by FINSEQ_1:47;
then n ^ <*the InitialSym of (TotalGrammar D)*> ==> n by A18, Th5;
then A23: n is_derivable_from n ^ <*the InitialSym of (TotalGrammar D)*> by Th7;
A24: S₁[ 0 ]

proof

let p be String of (TotalGrammar D); :: thesis: ( len p = 0 & p in D * implies p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> )
assume len p = 0 ; :: thesis: ( not p in D * or p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> )
then p = {} ;
then p ^ <*the InitialSym of (TotalGrammar D)*> = <*the InitialSym of (TotalGrammar D)*> by FINSEQ_1:47;
hence ( not p in D * or p ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> ) by Th6; :: thesis: verum

end;

A25: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A4);
len n = len n ;
then n ^ <*the InitialSym of (TotalGrammar D)*> is_derivable_from <*the InitialSym of (TotalGrammar D)*> by A25, A22;
then A26: n is_derivable_from <*the InitialSym of (TotalGrammar D)*> by A23, Th8;
rng a c= D ;
hence a in Lang (TotalGrammar D) by A19, A26; :: thesis: verum