theorem Th91:
for
m being
Element of
NAT for
S being non
empty non
void ManySortedSign for
o being
OperSymbol of
S for
Y being
infinite-yielding ManySortedSet of the
carrier of
S for
q being
Element of
Args (
o,
(Free (S,Y)))
for
s1,
s2 being
SortSymbol of
S for
V being
finite set st
m in dom q &
s1 = (the_arity_of o) /. m holds
ex
y being
Element of
Y . s1 ex
C being
context of
y ex
q1 being
Element of
Args (
o,
(Free (S,Y))) st
(
y nin V &
q1 = q +* (
m,
(y -term)) &
q1 is
y -context_including &
y -context_in q1 = y -term &
C = o -term q1 &
m = y -context_pos_in q1 &
transl C = transl (
o,
m,
q,
(Free (S,Y))) )