let G1, G2 be non empty strict DTConstrStr ; ( the carrier of G1 = F1() & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] ) ) & the carrier of G2 = F1() & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P1[x,p] ) ) implies G1 = G2 )
assume that
A1:
the carrier of G1 = F1()
and
A2:
for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] )
and
A3:
the carrier of G2 = F1()
and
A4:
for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P1[x,p] )
; G1 = G2
now for x, y being object holds
( ( [x,y] in the Rules of G1 implies [x,y] in the Rules of G2 ) & ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 ) )let x,
y be
object ;
( ( [x,y] in the Rules of G1 implies [x,y] in the Rules of G2 ) & ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 ) )hereby ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 )
assume A5:
[x,y] in the
Rules of
G1
;
[x,y] in the Rules of G2then A6:
y in the
carrier of
G1 *
by ZFMISC_1:87;
reconsider x1 =
x as
Symbol of
G1 by A5, ZFMISC_1:87;
reconsider y1 =
y as
FinSequence of the
carrier of
G1 by A6, FINSEQ_2:def 3;
A7:
(
x1 ==> y1 iff
P1[
x1,
y1] )
by A2;
reconsider x2 =
x as
Symbol of
G2 by A1, A3, A5, ZFMISC_1:87;
reconsider y2 =
y as
FinSequence of the
carrier of
G2 by A1, A3, A6, FINSEQ_2:def 3;
x2 ==> y2
by A4, A5, A7, LANG1:def 1;
hence
[x,y] in the
Rules of
G2
by LANG1:def 1;
verum
end; assume A8:
[x,y] in the
Rules of
G2
;
[x,y] in the Rules of G1then A9:
y in the
carrier of
G2 *
by ZFMISC_1:87;
reconsider x2 =
x as
Symbol of
G2 by A8, ZFMISC_1:87;
reconsider y2 =
y as
FinSequence of the
carrier of
G2 by A9, FINSEQ_2:def 3;
A10:
(
x2 ==> y2 iff
P1[
x2,
y2] )
by A4;
reconsider x1 =
x as
Symbol of
G1 by A1, A3, A8, ZFMISC_1:87;
reconsider y1 =
y as
FinSequence of the
carrier of
G1 by A1, A3, A9, FINSEQ_2:def 3;
x1 ==> y1
by A2, A8, A10, LANG1:def 1;
hence
[x,y] in the
Rules of
G1
by LANG1:def 1;
verum end;
hence
G1 = G2
by A1, A3, RELAT_1:def 2; verum