let t1, t2 be Element of (TermAlg S); ( ex F being ManySortedSet of S -Terms X st
( t1 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) & ex F being ManySortedSet of S -Terms X st
( t2 = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) implies t1 = t2 )
given F1 being ManySortedSet of S -Terms X such that A15:
t1 = F1 . t
and
A16:
for s being SortSymbol of S
for x being Element of X . s holds F1 . (root-tree [x,s]) = H2(x,s)
and
A17:
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F1 . ((Sym (o,X)) -tree p) = H3(o,F1 * p)
; ( for F being ManySortedSet of S -Terms X holds
( not t2 = F . t or ex s being SortSymbol of S ex x being Element of X . s st not F . (root-tree [x,s]) = root-tree [((w . s) . x),s] or ex o being OperSymbol of S ex p being ArgumentSeq of Sym (o,X) st not F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) or t1 = t2 )
given F2 being ManySortedSet of S -Terms X such that A18:
t2 = F2 . t
and
A19:
for s being SortSymbol of S
for x being Element of X . s holds F2 . (root-tree [x,s]) = H2(x,s)
and
A20:
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F2 . ((Sym (o,X)) -tree p) = H3(o,F2 * p)
; t1 = t2
F1 = F2
from MSAFREE4:sch 4(A16, A17, A19, A20);
hence
t1 = t2
by A15, A18; verum