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 )
assume A is MSAlgebra of E ; :: thesis: A is MSAlgebra of E +* S
then reconsider B = A as MSAlgebra of E ;
set T = E +* S;
A1: the carrier of (E +* S) = the carrier of E \/ the carrier of S by CIRCCOMB:def 2;
B is Algebra of S ;
then the carrier of S c= the carrier of E by Th59;
then A3: the carrier of (E +* S) = the carrier of E by A1, XBOOLE_1:12;
then reconsider Ss = the Sorts of B as ManySortedSet of ;
A4: the carrier' of (E +* S) = the carrier' of E \/ the carrier' of S by CIRCCOMB:def 2;
B is Algebra of S ;
then the carrier' of S c= the carrier' of E by Th59;
then A5: the carrier' of (E +* S) = the carrier' of E by A4, XBOOLE_1:12;
A6: ( dom the Arity of S = the carrier' of S & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1;
A7: ( the Arity of (E +* S) = the Arity of E +* the Arity of S & the ResultSort of (E +* S) = the ResultSort of E +* the ResultSort of S ) by CIRCCOMB:def 2;

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 A8: 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 A9: ( (Ss * the ResultSort of E) . i = Ss . (the ResultSort of E . i) & ((Ss # ) * the Arity of E) . i = (Ss # ) . (the Arity of E . i) ) by A5, FUNCT_2:21;
A10: ( (Ss * the ResultSort of (E +* S)) . i = Ss . (the ResultSort of (E +* S) . i) & ((Ss # ) * the Arity of (E +* S)) . i = (Ss # ) . (the Arity of (E +* S) . i) ) by A8, 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 S' = S as non void Signature ;
reconsider o = i as OperSymbol of S' by A12;
( B is Algebra of S' & the ResultSort of (E +* S) . o = the_result_sort_of o & the Arity of (E +* S) . o = the_arity_of o ) by A6, A7, 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 Th60; :: thesis: verum

end;

( 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 A6, A7, FUNCT_4:12;
hence the Charact of B . i is Function of (((Ss # ) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i) by A3, A5, A8, A9, A10, A11, 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 A5, PBOOLE:def 18;
set B' = MSAlgebra(# Ss,C #);
( the Sorts of MSAlgebra(# Ss,C #) = the Sorts of B & the Charact of MSAlgebra(# Ss,C #) = the Charact of B ) ;
then B is MSAlgebra of E +* S ;
hence A is MSAlgebra of E +* S ; :: thesis: verum