defpred S₁[ set , FinSequence] means ( P₁[$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₁() and
A2: for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff S₁[x,p] ) from DTCONSTR:sch 1();

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*>

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;

then A4: G is binary ;

now :: thesis: for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P₁[x,y,z] )

let x, y, z be Symbol of G; :: thesis: ( x ==> <*y,z*> iff P₁[x,y,z] )
reconsider yz = <*y,z*> as FinSequence of the carrier of G ;
( yz . 1 = y & yz . 2 = z ) ;
hence ( x ==> <*y,z*> iff P₁[x,y,z] ) by A2; :: thesis: verum

end;

hence ex G being non empty strict binary DTConstrStr st
( the carrier of G = F₁() & ( for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P₁[x,y,z] ) ) ) by A1, A4; :: thesis: verum