let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for x being Element of Args o,A holds (Den o,A) . x in the Sorts of A . (the_result_sort_of o)
let A be non-empty MSAlgebra of S; :: thesis: for o being OperSymbol of S
for x being Element of Args o,A holds (Den o,A) . x in the Sorts of A . (the_result_sort_of o)
let o be OperSymbol of S; :: thesis: for x being Element of Args o,A holds (Den o,A) . x in the Sorts of A . (the_result_sort_of o)
let x be Element of Args o,A; :: thesis: (Den o,A) . x in the Sorts of A . (the_result_sort_of o)
(Den o,A) . x is Element of the Sorts of A . (the ResultSort of S . o) by FUNCT_2:21;
hence (Den o,A) . x in the Sorts of A . (the_result_sort_of o) ; :: thesis: verum