let S be non empty Signature; :: thesis: for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra of E holds
A is MSAlgebra of E +* S
let A be Algebra of S; :: thesis: for E being non empty ManySortedSign st A is MSAlgebra of E holds
A is MSAlgebra of E +* S
let E be non empty ManySortedSign ; :: thesis: ( A is MSAlgebra of E implies A is MSAlgebra of E +* S )
set T = E +* S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
A2: the ResultSort of (E +* S) = the ResultSort of E +* the ResultSort of S by CIRCCOMB:def 2;
assume A is MSAlgebra of E ; :: thesis: A is MSAlgebra of E +* S
then reconsider B = A as MSAlgebra of E ;
A3: the Arity of (E +* S) = the Arity of E +* the Arity of S by CIRCCOMB:def 2;
B is Algebra of S ;
then A4: the carrier of S c= the carrier of E by Th59;
the carrier of (E +* S) = the carrier of E \/ the carrier of S by CIRCCOMB:def 2;
then A5: the carrier of (E +* S) = the carrier of E by A4, XBOOLE_1:12;
then reconsider Ss = the Sorts of B as ManySortedSet of the carrier of (E +* S) ;
B is Algebra of S ;
then A6: the carrier' of S c= the carrier' of E by Th59;
the carrier' of (E +* S) = the carrier' of E \/ the carrier' of S by CIRCCOMB:def 2;
then A7: the carrier' of (E +* S) = the carrier' of E by A6, XBOOLE_1:12;
A8: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;

now

let i be set ; :: thesis: ( i in the carrier' of (E +* S) implies the Charact of B . i is Function of (((Ss # ) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i) )
assume A9: i in the carrier' of (E +* S) ; :: thesis: the Charact of B . i is Function of (((Ss # ) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i)
then A10: (Ss * the ResultSort of (E +* S)) . i = Ss . (the ResultSort of (E +* S) . i) by FUNCT_2:21;

A11: now

assume A12: i in the carrier' of S ; :: thesis: the Charact of B . i is Function of ((the Sorts of B # ) . (the Arity of (E +* S) . i)),(the Sorts of B . (the ResultSort of (E +* S) . i))
then reconsider S9 = S as non void Signature ;
reconsider o = i as OperSymbol of S9 by A12;
A13: the Arity of (E +* S) . o = the_arity_of o by A8, A3, FUNCT_4:14;
the ResultSort of (E +* S) . o = the_result_sort_of o by A1, A2, FUNCT_4:14;
hence the Charact of B . i is Function of ((the Sorts of B # ) . (the Arity of (E +* S) . i)),(the Sorts of B . (the ResultSort of (E +* S) . i)) by A13, Th60; :: thesis: verum

end;

A14: ( not i in the carrier' of S implies ( the Arity of (E +* S) . i = the Arity of E . i & the ResultSort of (E +* S) . i = the ResultSort of E . i ) ) by A8, A1, A3, A2, FUNCT_4:12;
A15: ((Ss # ) * the Arity of E) . i = (Ss # ) . (the Arity of E . i) by A7, A9, FUNCT_2:21;
A16: ((Ss # ) * the Arity of (E +* S)) . i = (Ss # ) . (the Arity of (E +* S) . i) by A9, FUNCT_2:21;
(Ss * the ResultSort of E) . i = Ss . (the ResultSort of E . i) by A7, A9, FUNCT_2:21;
hence the Charact of B . i is Function of (((Ss # ) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i) by A5, A7, A9, A15, A10, A16, A11, A14, PBOOLE:def 18; :: thesis: verum

end;

then reconsider C = the Charact of B as ManySortedFunction of (Ss # ) * the Arity of (E +* S),Ss * the ResultSort of (E +* S) by A7, PBOOLE:def 18;
set B9 = MSAlgebra(# Ss,C #);
the Sorts of MSAlgebra(# Ss,C #) = the Sorts of B ;
then B is MSAlgebra of E +* S ;
hence A is MSAlgebra of E +* S ; :: thesis: verum