let S be non void Signature; :: thesis: for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
let E be non empty Signature; :: thesis: for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
let A be MSAlgebra over E; :: thesis: ( A is Algebra of S implies for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o)) )
A1: dom the Sorts of A = the carrier of E by PARTFUN1:def 2;
assume A is Algebra of S ; :: thesis: for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
let o be OperSymbol of S; :: thesis: the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
A3: dom the Sorts of B = the carrier of ES by PARTFUN1:def 2;
A4: S is Subsignature of ES by Def5;
then A5: the carrier' of S c= the carrier' of ES by INSTALG1:10;
the ResultSort of S = the ResultSort of ES | the carrier' of S by A4, INSTALG1:12;
then A6: the_result_sort_of o = the ResultSort of ES . o by FUNCT_1:49;
the Arity of S = the Arity of ES | the carrier' of S by A4, INSTALG1:12;
then A7: the_arity_of o = the Arity of ES . o by FUNCT_1:49;
A8: the Charact of B . o is Function of ((( the Sorts of B #) * the Arity of ES) . o),(( the Sorts of B * the ResultSort of ES) . o) by A5, PBOOLE:def 15;
the carrier' of ES = dom the ResultSort of ES by FUNCT_2:def 1;
then A9: ( the Sorts of B * the ResultSort of ES) . o = the Sorts of A . (the_result_sort_of o) by A5, A6, FUNCT_1:13;
the carrier' of ES = dom the Arity of ES by FUNCT_2:def 1;
then (( the Sorts of B #) * the Arity of ES) . o = ( the Sorts of A #) . (the_arity_of o) by A5, A3, A1, A7, FUNCT_1:13;
hence the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o)) by A9, A8; :: thesis: verum