let t1, t2 be Element of (TermAlg S); :: thesis: ( 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]) = H₂(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) = H₃(o,F1 * p) ; :: thesis: ( 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]) = H₂(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) = H₃(o,F2 * p) ; :: thesis: t1 = t2
F1 = F2 from MSAFREE4:sch 4(A16, A17, A19, A20);
hence t1 = t2 by A15, A18; :: thesis: verum