let I be set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) holds (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) holds (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for x being Element of Args o,(product A) holds (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
let o be OperSymbol of S; :: thesis: for x being Element of Args o,(product A) holds (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
let x be Element of Args o,(product A); :: thesis: (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
Result o,(product A) = (SORTS A) . (the_result_sort_of o) by PRALG_2:10
.= product (Carrier A,(the_result_sort_of o)) by PRALG_2:def 17 ;
hence (Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o)) ; :: thesis: verum