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