theorem Th113: :: MSAFREE5:111

for i being Nat
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))