let J be non empty non void Signature; :: thesis: for S being J -extension Signature
for T being MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

let S be J -extension Signature; :: thesis: for T being MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

let T be MSAlgebra over J; :: thesis: for I being set st I c= the carrier of S \ the carrier of J holds
for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

let I be set ; :: thesis: ( I c= the carrier of S \ the carrier of J implies for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X ) )

assume A1: I c= the carrier of S \ the carrier of J ; :: thesis: for X being ManySortedSet of I ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

let X be ManySortedSet of I; :: thesis: ex Q being MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )

set U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X;
A2: J is Subsignature of S by Def2;
dom (( the ManySortedSet of the carrier of S +* the Sorts of T) +* X) = (dom ( the ManySortedSet of the carrier of S +* the Sorts of T)) \/ (dom X) by FUNCT_4:def 1
.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ (dom X) by FUNCT_4:def 1
.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ I by PARTFUN1:def 2
.= ((dom the ManySortedSet of the carrier of S) \/ the carrier of J) \/ I by PARTFUN1:def 2
.= ( the carrier of S \/ the carrier of J) \/ I by PARTFUN1:def 2
.= the carrier of S \/ I by
.= the carrier of S by ;
then reconsider U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X as ManySortedSet of the carrier of S by ;
set C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T;
dom ( the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T) = (dom the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S) \/ (dom the Charact of T) by FUNCT_4:def 1
.= the carrier' of S \/ (dom the Charact of T) by PARTFUN1:def 2
.= the carrier' of S \/ the carrier' of J by PARTFUN1:def 2
.= the carrier' of S by ;
then reconsider C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T as ManySortedSet of the carrier' of S by ;
A3: ( dom X = I & I misses the carrier of J ) by ;
C is ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S
proof
let o be object ; :: according to PBOOLE:def 15 :: thesis: ( not o in the carrier' of S or C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] )
assume A4: o in the carrier' of S ; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]
then reconsider w = o as OperSymbol of S ;
per cases ( o in the carrier' of J or o nin the carrier' of J ) ;
suppose A5: o in the carrier' of J ; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]
then reconsider u = o as OperSymbol of J ;
o in dom the Charact of T by ;
then A6: C . o = the Charact of T . o by FUNCT_4:13;
( the Arity of J = the Arity of S | the carrier' of J & the ResultSort of J = the ResultSort of S | the carrier' of J ) by ;
then A7: ( the Arity of J . o = the Arity of S . o & the ResultSort of J . o = the ResultSort of S . o ) by ;
A8: ( ( the Sorts of T #) . () = product ( the Sorts of T * ()) & (U #) . () = product (U * ()) ) by FINSEQ_2:def 5;
A9: ( dom the Sorts of T = the carrier of J & rng () c= the carrier of J ) by PARTFUN1:def 2;
U * () = ( the ManySortedSet of the carrier of S +* the Sorts of T) * () by
.= the Sorts of T * () by ;
then A10: ( the Sorts of T #) . () = (U #) . () by A8;
A11: ( rng the ResultSort of S c= the carrier of S & rng the ResultSort of J c= the carrier of J & the carrier of J = dom the Sorts of T ) by PARTFUN1:def 2;
rng the ResultSort of J misses dom X by ;
then A12: U * the ResultSort of J = ( the ManySortedSet of the carrier of S +* the Sorts of T) * the ResultSort of J by FUNCT_7:11
.= the Sorts of T * the ResultSort of J by ;
( (( the Sorts of T #) * the Arity of J) . o = ( the Sorts of T #) . () & ((U #) * the Arity of S) . o = (U #) . () & ( the Sorts of T * the ResultSort of S) . o = the Sorts of T . ( the ResultSort of S . o) & ( the Sorts of T * the ResultSort of J) . o = the Sorts of T . ( the ResultSort of J . o) & (U * the ResultSort of S) . o = U . ( the ResultSort of S . o) & (U * the ResultSort of J) . o = U . ( the ResultSort of J . o) ) by ;
hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] by A6, A7, A10, A12; :: thesis: verum
end;
suppose o nin the carrier' of J ; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]
then o nin dom the Charact of T ;
then C . o = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S . o by FUNCT_4:11;
hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] ; :: thesis: verum
end;
end;
end;
then reconsider C = C as ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S ;
take Q = MSAlgebra(# U,C #); :: thesis: ( Q is T -extension & the Sorts of Q | I = X )
thus Q is T -extension :: thesis: the Sorts of Q | I = X
proof
A13: Q | J = Q | (J,(id the carrier of J),(id the carrier' of J)) by INSTALG1:def 4;
id the carrier of J, id the carrier' of J form_morphism_between J,S by ;
then ( the Sorts of (Q | J) = the Sorts of Q * (id the carrier of J) & the Charact of (Q | J) = the Charact of Q * (id the carrier' of J) ) by ;
then A14: ( the Sorts of (Q | J) = the Sorts of Q | the carrier of J & the Charact of (Q | J) = the Charact of Q | the carrier' of J ) by RELAT_1:65;
A15: ( dom the Sorts of T = the carrier of J & dom the Charact of T = the carrier' of J ) by PARTFUN1:def 2;
the Sorts of (Q | J) = ( the ManySortedSet of the carrier of S +* the Sorts of T) | the carrier of J by
.= the Sorts of T by A15 ;
hence Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) by ; :: according to AOFA_L00:def 19 :: thesis: verum
end;
dom X = I by PARTFUN1:def 2;
hence the Sorts of Q | I = X ; :: thesis: verum