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:3
.= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def 10 ;
hence (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) ; :: thesis: verum