let a, b be set ; :: thesis: ( a <> b implies Lang (IterGrammar a,b) = {b} * )
set T = IterGrammar a,b;
assume a <> b ; :: thesis: Lang (IterGrammar a,b) = {b} *
then A1: 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
A2: ( a = p & rng p c= Terminals (IterGrammar a,b) & p is_derivable_from <*the InitialSym of (IterGrammar a,b)*> ) ;
p is FinSequence of {b} by A1, A2, FINSEQ_1:def 4;
hence a in {b} * by A2, FINSEQ_1:def 11; :: thesis: verum

end;

A3: ( the carrier of (IterGrammar a,b) = {a,b} & the InitialSym of (IterGrammar a,b) = a & the Rules of (IterGrammar a,b) = {[a,<*b,a*>],[a,{} ]} ) by Def9;
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)*>;
A4: 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;

A5: 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 A6: 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 A7: ( len p = k + 1 & p in {b} * ) ; :: thesis: p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*>
then consider q being FinSequence, c being set such that
A8: ( p = q ^ <*c*> & len q = k ) by TREES_2:4;
p is FinSequence of {b} by A7, FINSEQ_1:def 11;
then A9: ( q is FinSequence of the carrier of (IterGrammar a,b) & q is FinSequence of {b} & <*c*> is FinSequence of the carrier of (IterGrammar a,b) & <*c*> is FinSequence of {b} & rng <*c*> = {c} ) by A8, FINSEQ_1:50, FINSEQ_1:55;
then reconsider q = q as String of (IterGrammar a,b) by FINSEQ_1:def 11;
q in {b} * by A9, FINSEQ_1:def 11;
then A10: q ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A6, A8;
A11: ( {c} c= {b} & {c} c= the carrier of (IterGrammar a,b) ) by A9, 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 A11, ZFMISC_1:37;
( [a,<*b,a*>] in the Rules of (IterGrammar a,b) & c = b ) by A3, TARSKI:def 1, TARSKI:def 2;
then the InitialSym of (IterGrammar a,b) ==> <*x,the InitialSym of (IterGrammar a,b)*> by A3, Def1;
then <*the InitialSym of (IterGrammar a,b)*> ==> <*x,the InitialSym of (IterGrammar a,b)*> by Th3;
then ( q ^ <*the InitialSym of (IterGrammar a,b)*> ==> q ^ <*x,the InitialSym of (IterGrammar a,b)*> & <*x,the InitialSym of (IterGrammar a,b)*> = <*x*> ^ <*the InitialSym of (IterGrammar a,b)*> ) by Th5, FINSEQ_1:def 9;
then q ^ <*the InitialSym of (IterGrammar a,b)*> ==> p ^ <*the InitialSym of (IterGrammar a,b)*> by A8, FINSEQ_1:45;
then p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from q ^ <*the InitialSym of (IterGrammar a,b)*> by Th7;
hence p ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A10, Th8; :: thesis: verum

end;

A12: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in {b} * or c in Lang (IterGrammar a,b) )
assume A13: c in {b} * ; :: thesis: c in Lang (IterGrammar a,b)
then reconsider c = c as FinSequence of {b} by FINSEQ_1:def 11;
A14: ( rng c c= {b} & {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 A3, FINSEQ_1:def 4;
then reconsider n = c as String of (IterGrammar a,b) by FINSEQ_1:def 11;
len n = len n ;
then A15: n ^ <*the InitialSym of (IterGrammar a,b)*> is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A12, A13;
A16: ( {} = {} the carrier of (IterGrammar a,b) & n ^ {} = n ) by FINSEQ_1:47;
[a,{} ] in the Rules of (IterGrammar a,b) by A3, TARSKI:def 2;
then the InitialSym of (IterGrammar a,b) ==> <*> the carrier of (IterGrammar a,b) by A3, Def1;
then <*the InitialSym of (IterGrammar a,b)*> ==> <*> the carrier of (IterGrammar a,b) by Th3;
then n ^ <*the InitialSym of (IterGrammar a,b)*> ==> n by A16, Th5;
then n is_derivable_from n ^ <*the InitialSym of (IterGrammar a,b)*> by Th7;
then n is_derivable_from <*the InitialSym of (IterGrammar a,b)*> by A15, Th8;
hence c in Lang (IterGrammar a,b) by A1, A14; :: thesis: verum