let S1, S2 be non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr ; :: thesis: ( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] & ( for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] & ( for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) implies S1 = S2 )
assume that
A24: ( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] ) and
A25: for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ; :: thesis: ( not Terminals S2 = SCM-Data-Loc or not NonTerminals S2 = [:1,5:] or ex x, y, z being Symbol of S2 st
( ( x ==> <*y,z*> implies x in [:1,5:] ) implies ( x in [:1,5:] & not x ==> <*y,z*> ) ) or S1 = S2 )
assume that
A26: ( Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] ) and
A27: for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ; :: thesis: S1 = S2
A28: the carrier of S1 = (Terminals S1) \/ (NonTerminals S1) by LANG1:1
.= the carrier of S2 by A24, A26, LANG1:1 ;
the Rules of S1 = the Rules of S2

proof

set p1 = the Rules of S1;
set p2 = the Rules of S2;
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in the Rules of S1 or [a,b] in the Rules of S2 ) & ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 ) )

hereby :: thesis: ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 )

assume A29: [a,b] in the Rules of S1 ; :: thesis: [a,b] in the Rules of S2
then reconsider l = a as Symbol of S1 by ZFMISC_1:87;
reconsider r = b as Element of the carrier of S1 * by A29, ZFMISC_1:87;
A30: l ==> r by A29, LANG1:def 1;
then consider x1, x2 being Symbol of S1 such that
A31: r = <*x1,x2*> by BINTREE1:def 4;
reconsider l = l, x1 = x1, x2 = x2 as Symbol of S2 by A28;
l in [:1,5:] by A25, A30, A31;
then l ==> <*x1,x2*> by A27;
hence [a,b] in the Rules of S2 by A31, LANG1:def 1; :: thesis: verum

end;

assume A32: [a,b] in the Rules of S2 ; :: thesis: [a,b] in the Rules of S1
then reconsider l = a as Symbol of S2 by ZFMISC_1:87;
reconsider r = b as Element of the carrier of S2 * by A32, ZFMISC_1:87;
A33: l ==> r by A32, LANG1:def 1;
then consider x1, x2 being Symbol of S2 such that
A34: r = <*x1,x2*> by BINTREE1:def 4;
reconsider l = l, x1 = x1, x2 = x2 as Symbol of S1 by A28;
l in [:1,5:] by A27, A33, A34;
then l ==> <*x1,x2*> by A25;
hence [a,b] in the Rules of S1 by A34, LANG1:def 1; :: thesis: verum

end;

hence S1 = S2 by A28; :: thesis: verum