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₁[ 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 object ; :: 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;
then A7: <* the InitialSym of (IterGrammar (a,b))*> ==> <*> the carrier of (IterGrammar (a,b)) by Th3;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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:3;
A14: rng <*c*> = {c} by FINSEQ_1:38;
A15: p is FinSequence of {b} by A11, FINSEQ_1:def 11;
then A16: q is FinSequence of {b} by A12, FINSEQ_1:36;
<*c*> is FinSequence of the carrier of (IterGrammar (a,b)) by A12, FINSEQ_1:36;
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:36;
then {c} c= {b} by A14, FINSEQ_1:def 4;
then reconsider c = c as Element of {b} by ZFMISC_1:31;
reconsider x = c as Symbol of (IterGrammar (a,b)) by A17, ZFMISC_1:31;
A18: q is FinSequence of the carrier of (IterGrammar (a,b)) by A12, FINSEQ_1:36;
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;
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:32;
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 object ; :: 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:7;
then rng c c= {a,b} ;
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:34;
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:34;
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 Nat holds S₁[k] from NAT_1:sch 2(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