let S be non empty non void ManySortedSign ; :: thesis: for o, a being set

for r being SortSymbol of S st o is_of_type <*a*>,r holds

for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let o, a be set ; :: thesis: for r being SortSymbol of S st o is_of_type <*a*>,r holds

for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let r be SortSymbol of S; :: thesis: ( o is_of_type <*a*>,r implies for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A1: ( the Arity of S . o = <*a*> & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

then A2: ( o in dom the Arity of S & dom the Arity of S c= the carrier' of S ) by FUNCT_1:def 2, RELAT_1:def 18;

then reconsider s = o as OperSymbol of S ;

let A be MSAlgebra over S; :: thesis: ( the Sorts of A . a <> {} & the Sorts of A . r <> {} implies for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A4: the Sorts of A . a <> {} ; :: thesis: ( not the Sorts of A . r <> {} or for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A5: the Sorts of A . r <> {} ; :: thesis: for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let x be Element of the Sorts of A . a; :: thesis: (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

A6: <*a*> = the_arity_of s by A1;

A7: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;

(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . <*a*> by A1, A2, FUNCT_2:15

.= product ( the Sorts of A * <*a*>) by A6, FINSEQ_2:def 5

.= product <*( the Sorts of A . a)*> by A6, FUNCT_7:18, A7, FINSEQ_2:34 ;

then A8: <*x*> in Args (s,A) by A4, FINSEQ_3:123;

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)) . <*x*> is Element of the Sorts of A . r by A1, A5, A8, FUNCT_2:5; :: thesis: verum

for r being SortSymbol of S st o is_of_type <*a*>,r holds

for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let o, a be set ; :: thesis: for r being SortSymbol of S st o is_of_type <*a*>,r holds

for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let r be SortSymbol of S; :: thesis: ( o is_of_type <*a*>,r implies for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A1: ( the Arity of S . o = <*a*> & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds

for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

then A2: ( o in dom the Arity of S & dom the Arity of S c= the carrier' of S ) by FUNCT_1:def 2, RELAT_1:def 18;

then reconsider s = o as OperSymbol of S ;

let A be MSAlgebra over S; :: thesis: ( the Sorts of A . a <> {} & the Sorts of A . r <> {} implies for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A4: the Sorts of A . a <> {} ; :: thesis: ( not the Sorts of A . r <> {} or for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r )

assume A5: the Sorts of A . r <> {} ; :: thesis: for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

let x be Element of the Sorts of A . a; :: thesis: (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r

A6: <*a*> = the_arity_of s by A1;

A7: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;

(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . <*a*> by A1, A2, FUNCT_2:15

.= product ( the Sorts of A * <*a*>) by A6, FINSEQ_2:def 5

.= product <*( the Sorts of A . a)*> by A6, FUNCT_7:18, A7, FINSEQ_2:34 ;

then A8: <*x*> in Args (s,A) by A4, FINSEQ_3:123;

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)) . <*x*> is Element of the Sorts of A . r by A1, A5, A8, FUNCT_2:5; :: thesis: verum