theorem Th35: :: MSATERM:35

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( 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 = q . i & vt is_an_evaluation_of t,f ) ) )