defpred S1[ set , FinSequence] means ( P1[$1,$2 . 1,$2 . 2] & $2 = <*($2 . 1),($2 . 2)*> );
consider G being non empty strict DTConstrStr such that
A1:
the carrier of G = F1()
and
A2:
for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff S1[x,p] )
from DTCONSTR:sch 1();
now 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;
for p being FinSequence st s ==> p holds
ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*>let p be
FinSequence;
( s ==> p implies ex pp1, pp2 being Symbol of G st p = <*pp1,pp2*> )assume A3:
s ==> p
;
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;
ex pp2 being Symbol of G st p = <*pp1,pp2*>take pp2 =
pp2;
p = <*pp1,pp2*>thus
p = <*pp1,pp2*>
by A2, A3;
verum end;
then A4:
G is binary
;
hence
ex G being non empty strict binary DTConstrStr st
( the carrier of G = F1() & ( for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P1[x,y,z] ) ) )
by A1, A4; verum