defpred S₁[ object ] means F₅() . $1 = F₆() . $1;
A5: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds S₁[ root-tree [x,s]]

proof

let s be SortSymbol of F₁(); :: thesis: for x being Element of F₂() . s holds S₁[ root-tree [x,s]]
let x be Element of F₂() . s; :: thesis: S₁[ root-tree [x,s]]
thus F₅() . (root-tree [x,s]) = F₃(x,s) by A1
.= F₆() . (root-tree [x,s]) by A3 ; :: thesis: verum

end;

A6: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) st ( for t being Term of F₁(),F₂() st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of F₁()] -tree p]

proof

let o be OperSymbol of F₁(); :: thesis: for p being ArgumentSeq of Sym (o,F₂()) st ( for t being Term of F₁(),F₂() st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of F₁()] -tree p]
let p be ArgumentSeq of Sym (o,F₂()); :: thesis: ( ( for t being Term of F₁(),F₂() st t in rng p holds
S₁[t] ) implies S₁[[o, the carrier of F₁()] -tree p] )
assume A7: for t being Term of F₁(),F₂() st t in rng p holds
S₁[t] ; :: thesis: S₁[[o, the carrier of F₁()] -tree p]
A8: ( dom (F₅() * p) = dom p & dom (F₆() * p) = dom p ) by PARTFUN1:def 2;

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

let x be object ; :: thesis: ( x in dom p implies (F₅() * p) . x = (F₆() * p) . x )
assume A9: x in dom p ; :: thesis: (F₅() * p) . x = (F₆() * p) . x
then reconsider i = x as Element of NAT ;
reconsider t = p . i as Term of F₁(),F₂() by A9, MSATERM:22;
t in rng p by A9, FUNCT_1:def 3;
then S₁[t] by A7;
hence (F₅() * p) . x = F₆() . t by A9, FUNCT_1:13
.= (F₆() * p) . x by A9, FUNCT_1:13 ;
:: thesis: verum

end;

then F₅() * p = F₆() * p by A8;
hence F₅() . ([o, the carrier of F₁()] -tree p) = F₄(o,(F₆() * p)) by A2
.= F₆() . ([o, the carrier of F₁()] -tree p) by A4 ;
:: thesis: verum

end;

A10: for t being Term of F₁(),F₂() holds S₁[t] from MSATERM:sch 1(A5, A6);
for x being object st x in F₁() -Terms F₂() holds
S₁[x] by A10;
hence F₅() = F₆() ; :: thesis: verum