defpred S_{1}[ set , FinSequence] means ( P_{1}[$1,$2 . 1,$2 . 2] & $2 = <*($2 . 1),($2 . 2)*> );

consider G being non empty strict DTConstrStr such that

A1: the carrier of G = F_{1}()
and

A2: for x being Symbol of G

for p being FinSequence of the carrier of G holds

( x ==> p iff S_{1}[x,p] )
from DTCONSTR:sch 1();

( the carrier of G = F_{1}() & ( for x, y, z being Symbol of G holds

( x ==> <*y,z*> iff P_{1}[x,y,z] ) ) )
by A1, A4; :: thesis: verum

consider G being non empty strict DTConstrStr such that

A1: the carrier of G = F

A2: for x being Symbol of G

for p being FinSequence of the carrier of G holds

( x ==> p iff S

now :: thesis: for s being Symbol of G

for p being FinSequence st s ==> p holds

ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

then A4:
G is binary
;for p being FinSequence st s ==> p holds

ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

let s be Symbol of G; :: thesis: for p being FinSequence st s ==> p holds

ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

let p be FinSequence; :: thesis: ( s ==> p implies ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> )

assume A3: s ==> p ; :: thesis: ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

then [s,p] in the Rules of G by LANG1:def 1;

then p in the carrier of G * by ZFMISC_1:87;

then reconsider pp = p as FinSequence of the carrier of G by FINSEQ_1:def 11;

pp = <*(pp . 1),(pp . 2)*> by A2, A3;

then rng pp = rng (<*(pp . 1)*> ^ <*(pp . 2)*>) by FINSEQ_1:def 9

.= (rng <*(pp . 1)*>) \/ (rng <*(pp . 2)*>) by FINSEQ_1:31

.= {(pp . 1)} \/ (rng <*(pp . 2)*>) by FINSEQ_1:39

.= {(pp . 1)} \/ {(pp . 2)} by FINSEQ_1:39

.= {(pp . 1),(pp . 2)} by ENUMSET1:1 ;

then ( pp . 1 in rng pp & pp . 2 in rng pp ) by TARSKI:def 2;

then reconsider pp1 = pp . 1, pp2 = pp . 2 as Symbol of G ;

take pp1 = pp1; :: thesis: ex pp2 being Symbol of G st p = <*pp1,pp2*>

take pp2 = pp2; :: thesis: p = <*pp1,pp2*>

thus p = <*pp1,pp2*> by A2, A3; :: thesis: verum

end;ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

let p be FinSequence; :: thesis: ( s ==> p implies ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> )

assume A3: s ==> p ; :: thesis: ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>

then [s,p] in the Rules of G by LANG1:def 1;

then p in the carrier of G * by ZFMISC_1:87;

then reconsider pp = p as FinSequence of the carrier of G by FINSEQ_1:def 11;

pp = <*(pp . 1),(pp . 2)*> by A2, A3;

then rng pp = rng (<*(pp . 1)*> ^ <*(pp . 2)*>) by FINSEQ_1:def 9

.= (rng <*(pp . 1)*>) \/ (rng <*(pp . 2)*>) by FINSEQ_1:31

.= {(pp . 1)} \/ (rng <*(pp . 2)*>) by FINSEQ_1:39

.= {(pp . 1)} \/ {(pp . 2)} by FINSEQ_1:39

.= {(pp . 1),(pp . 2)} by ENUMSET1:1 ;

then ( pp . 1 in rng pp & pp . 2 in rng pp ) by TARSKI:def 2;

then reconsider pp1 = pp . 1, pp2 = pp . 2 as Symbol of G ;

take pp1 = pp1; :: thesis: ex pp2 being Symbol of G st p = <*pp1,pp2*>

take pp2 = pp2; :: thesis: p = <*pp1,pp2*>

thus p = <*pp1,pp2*> by A2, A3; :: thesis: verum

now :: thesis: for x, y, z being Symbol of G holds

( x ==> <*y,z*> iff P_{1}[x,y,z] )

hence
ex G being non empty strict binary DTConstrStr st ( x ==> <*y,z*> iff P

let x, y, z be Symbol of G; :: thesis: ( x ==> <*y,z*> iff P_{1}[x,y,z] )

reconsider yz = <*y,z*> as FinSequence of the carrier of G ;

( yz . 1 = y & yz . 2 = z ) by FINSEQ_1:44;

hence ( x ==> <*y,z*> iff P_{1}[x,y,z] )
by A2; :: thesis: verum

end;reconsider yz = <*y,z*> as FinSequence of the carrier of G ;

( yz . 1 = y & yz . 2 = z ) by FINSEQ_1:44;

hence ( x ==> <*y,z*> iff P

( the carrier of G = F

( x ==> <*y,z*> iff P