let S be non empty Signature; :: thesis: for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
let A be Algebra of S; :: thesis: for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
let E be non empty ManySortedSign ; :: thesis: ( A is MSAlgebra over E implies A is MSAlgebra over 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 over E ; :: thesis: A is MSAlgebra over E +* S
then reconsider B = A as MSAlgebra over 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 Th57;
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 Th57;
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 :: thesis: for i being object st i in the carrier' of (E +* S) holds
the Charact of B . i is Function of (((Ss #) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i)
let i be object ; :: 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:15;
A11: now :: thesis: ( i in the carrier' of S implies 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)) )
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:13;
the ResultSort of (E +* S) . o = the_result_sort_of o by A1, A2, FUNCT_4:13;
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, Th58; :: 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:11;
A15: ((Ss #) * the Arity of E) . i = (Ss #) . ( the Arity of E . i) by A7, A9, FUNCT_2:15;
A16: ((Ss #) * the Arity of (E +* S)) . i = (Ss #) . ( the Arity of (E +* S) . i) by A9, FUNCT_2:15;
(Ss * the ResultSort of E) . i = Ss . ( the ResultSort of E . i) by A7, A9, FUNCT_2:15;
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 15; :: 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 15;
set B9 = MSAlgebra(# Ss,C #);
the Sorts of MSAlgebra(# Ss,C #) = the Sorts of B ;
then B is MSAlgebra over E +* S ;
hence A is MSAlgebra over E +* S ; :: thesis: verum