let G1, G2 be strict GrammarStr ; :: thesis: ( the carrier of G1 = {a} & the Rules of G1 = {[a,{} ]} & the carrier of G2 = {a} & the Rules of G2 = {[a,{} ]} implies G1 = G2 )
assume that
A1: ( the carrier of G1 = {a} & the Rules of G1 = {[a,{} ]} ) and
A2: ( the carrier of G2 = {a} & the Rules of G2 = {[a,{} ]} ) ; :: thesis: G1 = G2
( the InitialSym of G1 = a & the InitialSym of G2 = a & G1 = GrammarStr(# the carrier of G1,the InitialSym of G1,the Rules of G1 #) & G2 = GrammarStr(# the carrier of G2,the InitialSym of G2,the Rules of G2 #) ) by A1, A2, TARSKI:def 1;
hence G1 = G2 by A1, A2; :: thesis: verum