defpred S1[ set ] means F5() . $1 = F6() . $1;
A5:
for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be
Symbol of
F1();
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS F1();
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A6:
nt ==> roots ts
and A7:
for
t being
DecoratedTree of the
carrier of
F1() st
t in rng ts holds
F5()
. t = F6()
. t
;
S1[nt -tree ts]
A8:
rng ts c= TS F1()
by FINSEQ_1:def 4;
then A9:
rng ts c= dom F5()
by FUNCT_2:def 1;
then A10:
dom (F5() * ts) = dom ts
by RELAT_1:27;
rng ts c= dom F6()
by A8, FUNCT_2:def 1;
then A11:
dom (F6() * ts) = dom ts
by RELAT_1:27;
dom (F5() * ts) =
dom ts
by A9, RELAT_1:27
.=
Seg (len ts)
by FINSEQ_1:def 3
;
then reconsider ntv1 =
F5()
* ts as
FinSequence by FINSEQ_1:def 2;
rng ntv1 c= F2()
by RELAT_1:def 19;
then
ntv1 is
FinSequence of
F2()
by FINSEQ_1:def 4;
then reconsider ntv1 =
ntv1 as
Element of
F2()
* by FINSEQ_1:def 11;
reconsider tss =
ts as
Element of
(TS F1()) * by FINSEQ_1:def 11;
thus F5()
. (nt -tree ts) =
F4(
nt,
tss,
ntv1)
by A2, A6
.=
F6()
. (nt -tree ts)
by A4, A6, A10, A11, A12, FUNCT_1:2
;
verum
end;
A15:
for s being Symbol of F1() st s in Terminals F1() holds
S1[ root-tree s]
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
S1[t]
from DTCONSTR:sch 7(A15, A5);
then
for x being object st x in TS F1() holds
F5() . x = F6() . x
;
hence
F5() = F6()
by FUNCT_2:12; verum