let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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:15;
hence (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ; :: thesis: verum