let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for r being SortSymbol of S st o is_of_type {} ,r holds
for A being MSAlgebra over S st the Sorts of A . r <> {} holds
(Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r
let o be OperSymbol of S; :: thesis: for r being SortSymbol of S st o is_of_type {} ,r holds
for A being MSAlgebra over S st the Sorts of A . r <> {} holds
(Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r
let r be SortSymbol of S; :: thesis: ( o is_of_type {} ,r implies for A being MSAlgebra over S st the Sorts of A . r <> {} holds
(Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r )
assume A1: ( the Arity of S . o = {} & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: for A being MSAlgebra over S st the Sorts of A . r <> {} holds
(Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r
reconsider s = o as OperSymbol of S ;
let A be MSAlgebra over S; :: thesis: ( the Sorts of A . r <> {} implies (Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r )
assume A3: the Sorts of A . r <> {} ; :: thesis: (Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r
A4: <*> the carrier of S in the carrier of S * by FINSEQ_1:def 11;
(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . {} by A1, FUNCT_2:15
.= product ( the Sorts of A * {}) by A4, FINSEQ_2:def 5
.= product {} ;
then A5: {} in Args (s,A) by CARD_3:10, TARSKI:def 1;
Result (s,A) = the Sorts of A . (the_result_sort_of s) by FUNCT_2:15;
hence (Den ((In (o, the carrier' of S)),A)) . {} is Element of the Sorts of A . r by A1, A3, A5, FUNCT_2:5; :: thesis: verum