let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let A be non-empty MSAlgebra of S; :: thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let V be Variables of A; :: thesis: for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let t be c-Term of A,V; :: thesis: for f being ManySortedFunction of V,the Sorts of A
for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
let f be ManySortedFunction of V,the Sorts of A; :: thesis: for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2
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

let s be SortSymbol of S; :: thesis: for x being Element of the Sorts of A . s holds S₁[x -term A,V]
let x be Element of the Sorts of A . s; :: thesis: S₁[x -term A,V]
thus S₁[x -term A,V] :: thesis: verum

proof

set t = x -term A,V;
let e1, e2 be finite DecoratedTree; :: thesis: ( e1 is_an_evaluation_of x -term A,V,f & e2 is_an_evaluation_of x -term A,V,f implies e1 = e2 )
assume A2: ( e1 is_an_evaluation_of x -term A,V,f & e2 is_an_evaluation_of x -term A,V,f ) ; :: thesis: e1 = e2
then A3: ( dom e1 = dom (x -term A,V) & dom e2 = dom (x -term A,V) & x -term A,V = root-tree [x,s] & dom (root-tree [x,s]) = elementary_tree 0 & (root-tree [x,s]) . {} = [x,s] ) by Def9, TREES_4:3;
{} is Node of e1 by TREES_1:47;
then ( e1 . {} = x & e2 . {} = x ) by A2, A3, Def9;
then ( e1 = root-tree x & e2 = root-tree x ) by A3, TREES_4:5;
hence e1 = e2 ; :: thesis: verum

end;

end;

A4: now

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

proof

set t = v -term A;
let e1, e2 be finite DecoratedTree; :: thesis: ( e1 is_an_evaluation_of v -term A,f & e2 is_an_evaluation_of v -term A,f implies e1 = e2 )
assume A5: ( e1 is_an_evaluation_of v -term A,f & e2 is_an_evaluation_of v -term A,f ) ; :: thesis: e1 = e2
then A6: ( dom e1 = dom (v -term A) & dom e2 = dom (v -term A) & v -term A = root-tree [v,s] & dom (root-tree [v,s]) = elementary_tree 0 & (root-tree [v,s]) . {} = [v,s] ) by Def9, TREES_4:3;
{} is Node of e1 by TREES_1:47;
then ( e1 . {} = (f . s) . v & e2 . {} = (f . s) . v ) by A5, A6, Def9;
then ( e1 = root-tree ((f . s) . v) & e2 = root-tree ((f . s) . v) ) by A6, TREES_4:5;
hence e1 = e2 ; :: thesis: verum

end;

end;

A7: now

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

proof

let e1, e2 be finite DecoratedTree; :: thesis: ( e1 is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f & e2 is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f implies e1 = e2 )
set t = (Sym o,(the Sorts of A \/ V)) -tree p;
assume A9: ( e1 is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f & e2 is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f ) ; :: thesis: e1 = e2
then consider q1 being DTree-yielding FinSequence such that
A10: ( len q1 = len p & e1 = ((Den o,A) . (roots q1)) -tree q1 & ( 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 Th35;
consider q2 being DTree-yielding FinSequence such that
A11: ( len q2 = len p & e2 = ((Den o,A) . (roots q2)) -tree q2 & ( 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 A9, Th35;

A12: now

let i be Element of NAT ; :: thesis: ( i < len p implies q1 . (i + 1) = q2 . (i + 1) )
assume A13: i < len p ; :: thesis: q1 . (i + 1) = q2 . (i + 1)
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A14: i + 1 in dom p by A13, Lm9;
then consider vt1 being finite DecoratedTree such that
A15: ( vt1 = q1 . (i + 1) & vt1 is_an_evaluation_of t,f ) by A10;
consider vt2 being finite DecoratedTree such that
A16: ( vt2 = q2 . (i + 1) & vt2 is_an_evaluation_of t,f ) by A11, A14;
t in rng p by A13, Lm9;
hence q1 . (i + 1) = q2 . (i + 1) by A8, A15, A16; :: thesis: verum

end;

A17: ( dom q1 = Seg (len q1) & dom q2 = Seg (len q2) ) by FINSEQ_1:def 3;

now

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

end;

then q1 = q2 by A10, A11, A17, FINSEQ_1:17;
hence e1 = e2 by A10, A11; :: thesis: verum

end;

end;

for t being c-Term of A,V holds S₁[t] from MSATERM:sch 3(A1, A4, A7);
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: verum