defpred S₁[ set ] means F₅() . $1 = F₆() . $1;
A5: for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F₁() st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]

proof

let nt be Symbol of F₁(); :: thesis: for ts being FinSequence of TS F₁() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F₁() st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]
let ts be FinSequence of TS F₁(); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F₁() st t in rng ts holds
S₁[t] ) implies S₁[nt -tree ts] )
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of F₁() st t in rng ts holds
F₅() . t = F₆() . t ; :: thesis: S₁[nt -tree ts]
A8: rng ts c= TS F₁() by FINSEQ_1:def 4;
then A9: rng ts c= dom F₅() by FUNCT_2:def 1;
then A10: dom (F₅() * ts) = dom ts by RELAT_1:27;
rng ts c= dom F₆() by A8, FUNCT_2:def 1;
then A11: dom (F₆() * ts) = dom ts by RELAT_1:27;

A12: now :: thesis: for x being object st x in dom ts holds
(F₅() * ts) . x = (F₆() * ts) . x

let x be object ; :: thesis: ( x in dom ts implies (F₅() * ts) . x = (F₆() * ts) . x )
assume A13: x in dom ts ; :: thesis: (F₅() * ts) . x = (F₆() * ts) . x
then reconsider t = ts . x as Element of FinTrees the carrier of F₁() by DTCONSTR:2;
t in rng ts by A13, FUNCT_1:def 3;
then A14: F₅() . t = F₆() . t by A7;
thus (F₅() * ts) . x = F₅() . t by A10, A13, FUNCT_1:12
.= (F₆() * ts) . x by A11, A13, A14, FUNCT_1:12 ; :: thesis: verum

end;

dom (F₅() * ts) = dom ts by A9, RELAT_1:27
.= Seg (len ts) by FINSEQ_1:def 3 ;
then reconsider ntv1 = F₅() * ts as FinSequence by FINSEQ_1:def 2;
rng ntv1 c= F₂() by RELAT_1:def 19;
then ntv1 is FinSequence of F₂() by FINSEQ_1:def 4;
then reconsider ntv1 = ntv1 as Element of F₂() * by FINSEQ_1:def 11;
reconsider tss = ts as Element of (TS F₁()) * by FINSEQ_1:def 11;
thus F₅() . (nt -tree ts) = F₄(nt,tss,ntv1) by A2, A6
.= F₆() . (nt -tree ts) by A4, A6, A10, A11, A12, FUNCT_1:2 ; :: thesis: verum

end;

A15: for s being Symbol of F₁() st s in Terminals F₁() holds
S₁[ root-tree s]

proof

let s be Symbol of F₁(); :: thesis: ( s in Terminals F₁() implies S₁[ root-tree s] )
assume A16: s in Terminals F₁() ; :: thesis: S₁[ root-tree s]
hence F₅() . (root-tree s) = F₃(s) by A1
.= F₆() . (root-tree s) by A3, A16 ;
:: thesis: verum

end;

for t being DecoratedTree of the carrier of F₁() st t in TS F₁() holds
S₁[t] from DTCONSTR:sch 7(A15, A5);
then for x being object st x in TS F₁() holds
F₅() . x = F₆() . x ;
hence F₅() = F₆() by FUNCT_2:12; :: thesis: verum