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

( 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

hence
S1 = S2
by A28; :: thesis: verum
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 ) )

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;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 A32:
[a,b] in the Rules of S2
; :: thesis: [a,b] in the Rules of S1assume 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;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

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