thus for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = {0,1} & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff S₁[x,p] ) ) & the carrier of G2 = {0,1} & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff S₁[x,p] ) ) holds
G1 = G2 from DTCONSTR:sch 2(); :: thesis: verum