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