let S be non empty non void ManySortedSign ; :: thesis: for o, a, b being set
for r being SortSymbol of S st o is_of_type <*a,b*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . b <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
let o, a, b be set ; :: thesis: for r being SortSymbol of S st o is_of_type <*a,b*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . b <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
let r be SortSymbol of S; :: thesis: ( o is_of_type <*a,b*>,r implies for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . b <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r )
assume A1: ( the Arity of S . o = <*a,b*> & 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 . b <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> 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 . b <> {} & the Sorts of A . r <> {} implies for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r )
assume A4: the Sorts of A . a <> {} ; :: thesis: ( not the Sorts of A . b <> {} or not the Sorts of A . r <> {} or for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r )
assume A5: the Sorts of A . b <> {} ; :: thesis: ( not the Sorts of A . r <> {} or for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r )
assume A6: the Sorts of A . r <> {} ; :: thesis: for x being Element of the Sorts of A . a
for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
let x be Element of the Sorts of A . a; :: thesis: for y being Element of the Sorts of A . b holds (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
let y be Element of the Sorts of A . b; :: thesis: (Den ((In (o, the carrier' of S)),A)) . <*x,y*> is Element of the Sorts of A . r
A7: <*a,b*> = the_arity_of s by A1;
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
then A8: ( the Sorts of A is Function of the carrier of S,(rng the Sorts of A) & rng the Sorts of A <> {} ) by FUNCT_2:2;
(( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . <*a,b*> by A1, A2, FUNCT_2:15
.= product ( the Sorts of A * <*a,b*>) by A7, FINSEQ_2:def 5
.= product <*( the Sorts of A . a),( the Sorts of A . b)*> by A7, A8, FINSEQ_2:36 ;
then A9: <*x,y*> in Args (s,A) by A4, A5, FINSEQ_3:124;
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,y*> is Element of the Sorts of A . r by A1, A6, A9, FUNCT_2:5; :: thesis: verum