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

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