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 = () \/ () by LANG1:1
.= the carrier of S2 by ;
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 ;
A30: l ==> r by ;
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 ;
then l ==> <*x1,x2*> by A27;
hence [a,b] in the Rules of S2 by ; :: 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 ;
A33: l ==> r by ;
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 ;
then l ==> <*x1,x2*> by A25;
hence [a,b] in the Rules of S1 by ; :: thesis: verum
end;
hence S1 = S2 by A28; :: thesis: verum