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

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