set G = F₁();
defpred S₁[ set ] means F₅() . $1 = F₆() . $1;

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

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

end;

A5: now :: thesis: 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]

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
S₁[t] ; :: thesis: S₁[nt -tree ts]
A8: rng ts c= TS F₁() by FINSEQ_1:def 4;
then rng ts c= dom F₅() by FUNCT_2:def 1;
then A9: dom (F₅() * ts) = dom ts by RELAT_1:27;
reconsider ntv1 = F₅() * ts as FinSequence ;
reconsider ntv1 = ntv1 as FinSequence of F₂() ;
rng ts c= dom F₆() by A8, FUNCT_2:def 1;
then A10: dom (F₆() * ts) = dom ts by RELAT_1:27;

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 A11: 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 Th2;
t in rng ts by A11, FUNCT_1:def 3;
then A12: F₅() . t = F₆() . t by A7;
thus (F₅() * ts) . x = F₅() . t by A9, A11, FUNCT_1:12
.= (F₆() * ts) . x by A10, A11, A12, FUNCT_1:12 ; :: thesis: verum

end;

then A13: F₅() * ts = F₆() * ts by A9, A10, FUNCT_1:2;
F₅() . (nt -tree ts) = F₄(nt,(roots ts),ntv1) by A1, A6
.= F₆() . (nt -tree ts) by A2, A6, A13 ;
hence S₁[nt -tree ts] ; :: thesis: verum

end;

for t being DecoratedTree of the carrier of F₁() st t in TS F₁() holds
S₁[t] from DTCONSTR:sch 7(A3, 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