let a, b be set ; :: thesis: ( a <> b implies Lang (IterGrammar a,b) = {b} * )
set T = IterGrammar a,b;
set I = <*the InitialSym of (IterGrammar a,b)*>;
defpred S₁[ Element of NAT ] means for p being String of (IterGrammar a,b) st len p = $1 & p in {b} * holds
p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*>;
A1: the carrier of (IterGrammar a,b) = {a,b} by Def9;
assume a <> b ; :: thesis: Lang (IterGrammar a,b) = {b} *
then A2: Terminals (IterGrammar a,b) = {b} by Th14;
thus Lang (IterGrammar a,b) c= {b} * :: according to XBOOLE_0:def 10 :: thesis: {b} * c= Lang (IterGrammar a,b)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Lang (IterGrammar a,b) or a in {b} * )
assume a in Lang (IterGrammar a,b) ; :: thesis: a in {b} *
then consider p being String of (IterGrammar a,b) such that
A3: a = p and
A4: rng p c= Terminals (IterGrammar a,b) and
p is_derivable_from <*the InitialSym of (IterGrammar a,b)*> ;
p is FinSequence of {b} by A2, A4, FINSEQ_1:def 4;
hence a in {b} * by A3, FINSEQ_1:def 11; :: thesis: verum

end;

A5: the InitialSym of (IterGrammar a,b) = a by Def9;
A6: the Rules of (IterGrammar a,b) = {[a,<*b,a*>],[a,{} ]} by Def9;
then [a,{} ] in the Rules of (IterGrammar a,b) by TARSKI:def 2;
then the InitialSym of (IterGrammar a,b) ==> <*> the carrier of (IterGrammar a,b) by A5, Def1;
then A7: <*the InitialSym of (IterGrammar a,b)*> ==> <*> the carrier of (IterGrammar a,b) by Th3;
A8: 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 A9: for p being String of (IterGrammar a,b) st len p = k & p in {b} * holds
p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> ; :: thesis: S₁[k + 1]
let p be String of (IterGrammar a,b); :: thesis: ( len p = k + 1 & p in {b} * implies p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> )
assume that
A10: len p = k + 1 and
A11: p in {b} * ; :: thesis: p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*>
consider q being FinSequence, c being set such that
A12: p = q ^ <*c*> and
A13: len q = k by A10, TREES_2:4;
A14: rng <*c*> = {c} by FINSEQ_1:55;
A15: p is FinSequence of {b} by A11, FINSEQ_1:def 11;
then A16: q is FinSequence of {b} by A12, FINSEQ_1:50;
<*c*> is FinSequence of the carrier of (IterGrammar a,b) by A12, FINSEQ_1:50;
then A17: {c} c= the carrier of (IterGrammar a,b) by A14, FINSEQ_1:def 4;
<*c*> is FinSequence of {b} by A12, A15, FINSEQ_1:50;
then {c} c= {b} by A14, FINSEQ_1:def 4;
then reconsider c = c as Element of {b} by ZFMISC_1:37;
reconsider x = c as Symbol of (IterGrammar a,b) by A17, ZFMISC_1:37;
A18: q is FinSequence of the carrier of (IterGrammar a,b) by A12, FINSEQ_1:50;
A19: [a,<*b,a*>] in the Rules of (IterGrammar a,b) by A6, TARSKI:def 2;
reconsider q = q as String of (IterGrammar a,b) by A18, FINSEQ_1:def 11;
c = b by TARSKI:def 1;
then the InitialSym of (IterGrammar a,b) ==> <*x,the InitialSym of (IterGrammar a,b)*> by A5, A19, Def1;
then <*the InitialSym of (IterGrammar a,b)*> ==> <*x,the InitialSym of (IterGrammar a,b)*> by Th3;
then A20: q ^ <*the InitialSym of (IterGrammar a,b)*> ==> q ^ <*x,the InitialSym of (IterGrammar a,b)*> by Th5;
<*x,the InitialSym of (IterGrammar a,b)*> = <*x*> ^ <*the InitialSym of (IterGrammar a,b)*> by FINSEQ_1:def 9;
then q ^ <*the InitialSym of (IterGrammar a,b)*> ==> p ^ <*the InitialSym of (IterGrammar a,b)*> by A12, A20, FINSEQ_1:45;
then A21: p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from q ^ <*the InitialSym of (IterGrammar a,b)*> by Th7;
q in {b} * by A16, FINSEQ_1:def 11;
then q ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A9, A13;
hence p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A21, Th8; :: thesis: verum

end;

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

proof

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

end;

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