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