theorem
for
S being non
empty non
void ManySortedSign for
X0 being
V5()
countable ManySortedSet of
S for
A0 being
b2,
b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over
S for
w being
ManySortedFunction of
X0, the
carrier of
S --> NAT for
o being
OperSymbol of
S for
p being
Element of
Args (
o,
(Free (S,X0)))
for
q being
Element of
Args (
o,
A0) st
(canonical_homomorphism A0) # p = q holds
for
t1,
t2 being
Term of
S,
X0 st
t1 = (Den (o,(Free (S,X0)))) . p &
t2 = (Den (o,A0)) . q holds
for
t3,
t4 being
Element of
(TermAlg S),
(the_result_sort_of o) st
t3 = # (
t1,
w) &
t4 = # (
t2,
w) holds
A0 |= t3 '=' t4