let S be non void Signature; 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; 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; ( 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
; 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; 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; verum