let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra over S; :: thesis:
let V be Variables of A; :: thesis:
let t be c-Term of A,V; :: thesis:
let f be ManySortedFunction of V, the Sorts of A; :: thesis:
defpred S₁[ c-Term of A,V] means for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of $1,f & e2 is_an_evaluation_of $1,f holds
e1 = e2;

A1: now :: thesis:

let s be SortSymbol of S; :: thesis:
let v be Element of V . s; :: thesis:
thus S₁[v -term A] :: thesis:

proof

let e1, e2 be finite DecoratedTree; :: thesis:
set t = v -term A;
assume that
A2: e1 is_an_evaluation_of v -term A,f and
A3: e2 is_an_evaluation_of v -term A,f ; :: thesis:
A4: dom e1 = dom (v -term A) by A2;
A5: {} is Node of e1 by TREES_1:22;
A6: (root-tree [v,s]) . {} = [v,s] by TREES_4:3;
then e1 . {} = (f . s) . v by A2, A5;
then A7: e1 = root-tree ((f . s) . v) by A4, TREES_4:3, TREES_4:5;
A8: dom e2 = dom (v -term A) by A3;
e2 . {} = (f . s) . v by A3, A4, A6, A5;
hence e1 = e2 by A8, A7, TREES_4:3, TREES_4:5; :: thesis:

end;

end;

A9: now :: thesis:

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of o,A,V; :: thesis:
assume A10: for t being c-Term of A,V st t in rng p holds
S₁[t] ; :: thesis:
thus S₁[(Sym (o,( the Sorts of A (\/) V))) -tree p] :: thesis:

proof

set t = (Sym (o,( the Sorts of A (\/) V))) -tree p;
let e1, e2 be finite DecoratedTree; :: thesis:
assume that
A11: e1 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f and
A12: e2 is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f ; :: thesis:
consider q1 being DTree-yielding FinSequence such that
A13: len q1 = len p and
A14: e1 = ((Den (o,A)) . (roots q1)) -tree q1 and
A15: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q1 . i & vt is_an_evaluation_of t,f ) by A11, Th35;
consider q2 being DTree-yielding FinSequence such that
A16: len q2 = len p and
A17: e2 = ((Den (o,A)) . (roots q2)) -tree q2 and
A18: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q2 . i & vt is_an_evaluation_of t,f ) by A12, Th35;

A19: now :: thesis:

let i be Element of NAT ; :: thesis:
assume A20: i < len p ; :: thesis:
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A21: ex vt2 being finite DecoratedTree st
( vt2 = q2 . (i + 1) & vt2 is_an_evaluation_of t,f ) by A18, A20, Lm9;
ex vt1 being finite DecoratedTree st
( vt1 = q1 . (i + 1) & vt1 is_an_evaluation_of t,f ) by A15, A20, Lm9;
hence q1 . (i + 1) = q2 . (i + 1) by A10, A20, A21, Lm9; :: thesis:

end;

A22: now :: thesis:

let i be Nat; :: thesis:
assume i in dom q1 ; :: thesis:
then ex k being Element of NAT st
( i = k + 1 & k < len q1 ) by Lm1;
hence q1 . i = q2 . i by A13, A19; :: thesis:

end;

A23: dom q2 = Seg (len q2) by FINSEQ_1:def 3;
dom q1 = Seg (len q1) by FINSEQ_1:def 3;
then q1 = q2 by A13, A16, A23, A22, FINSEQ_1:13;
hence e1 = e2 by A14, A17; :: thesis:

end;

end;

A24: now :: thesis:

let s be SortSymbol of S; :: thesis:
let x be Element of the Sorts of A . s; :: thesis:
thus S₁[x -term (A,V)] :: thesis:

proof

let e1, e2 be finite DecoratedTree; :: thesis:
set t = x -term (A,V);
assume that
A25: e1 is_an_evaluation_of x -term (A,V),f and
A26: e2 is_an_evaluation_of x -term (A,V),f ; :: thesis:
A27: dom e1 = dom (x -term (A,V)) by A25;
A28: {} is Node of e1 by TREES_1:22;
A29: (root-tree [x,s]) . {} = [x,s] by TREES_4:3;
then e1 . {} = x by A25, A28;
then A30: e1 = root-tree x by A27, TREES_4:3, TREES_4:5;
A31: dom e2 = dom (x -term (A,V)) by A26;
e2 . {} = x by A26, A27, A29, A28;
hence e1 = e2 by A31, A30, TREES_4:3, TREES_4:5; :: thesis:

end;

end;

for t being c-Term of A,V holds S₁[t] from MSATERM:sch 3(A24, A1, A9);
hence for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2 ; :: thesis: