let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a being set
for r being SortSymbol of S st o is_of_type a,r holds
( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
let A be non-empty MSAlgebra over S; :: thesis: for o being OperSymbol of S
for a being set
for r being SortSymbol of S st o is_of_type a,r holds
( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
let o be OperSymbol of S; :: thesis: for a being set
for r being SortSymbol of S st o is_of_type a,r holds
( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
let a be set ; :: thesis: for r being SortSymbol of S st o is_of_type a,r holds
( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
let r be SortSymbol of S; :: thesis: ( o is_of_type a,r implies ( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = 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: ( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
then A2: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . a by FUNCT_2:15;
( the Sorts of A * the ResultSort of S) . o = the Sorts of A . r by A1, FUNCT_2:15;
hence Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) by A2; :: thesis: ( Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )
thus ( Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r ) by A1, FUNCT_2:15; :: thesis: verum