let S be non void Signature; :: thesis: for E being non empty Signature
for A being MSAlgebra of 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 of 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 of 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)) )
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
A1: A is feasible MSAlgebra of ES by Def7;
reconsider B = A as MSAlgebra of ES by A1;
A2: S is Subsignature of ES by Def5;
then A3: ( the Arity of S = the Arity of ES | the carrier' of S & the ResultSort of S = the ResultSort of ES | the carrier' of S ) by INSTALG1:13;
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))
A4: ( o in the carrier' of S & the carrier' of S c= the carrier' of ES ) by A2, INSTALG1:11;
A5: ( the carrier' of ES = dom the Arity of ES & the carrier' of ES = dom the ResultSort of ES ) by FUNCT_2:def 1;
A6: ( dom the Sorts of B = the carrier of ES & dom the Sorts of A = the carrier of E ) by PARTFUN1:def 4;
the_arity_of o = the Arity of ES . o by A3, FUNCT_1:72;
then A7: ((the Sorts of B # ) * the Arity of ES) . o = (the Sorts of A # ) . (the_arity_of o) by A4, A5, A6, FUNCT_1:23;
the_result_sort_of o = the ResultSort of ES . o by A3, FUNCT_1:72;
then A8: (the Sorts of B * the ResultSort of ES) . o = the Sorts of A . (the_result_sort_of o) by A4, A5, FUNCT_1:23;
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 A4, PBOOLE:def 18;
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 A7, A8; :: thesis: verum