let J be non empty non void Signature; :: thesis: for S being J -extension Signature
for T being non-empty MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being non-empty ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
let S be J -extension Signature; :: thesis: for T being non-empty MSAlgebra over J
for I being set st I c= the carrier of S \ the carrier of J holds
for X being non-empty ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
let T be non-empty MSAlgebra over J; :: thesis: for I being set st I c= the carrier of S \ the carrier of J holds
for X being non-empty ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
set K = the carrier of S \ the carrier of J;
let I be set ; :: thesis: ( I c= the carrier of S \ the carrier of J implies for X being non-empty ManySortedSet of I ex Q being non-empty 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 non-empty ManySortedSet of I ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
let X be non-empty ManySortedSet of I; :: thesis: ex Q being non-empty MSAlgebra over S st
( Q is T -extension & the Sorts of Q | I = X )
set Y = the non-empty ManySortedSet of the carrier of S \ the carrier of J +* X;
dom ( the non-empty ManySortedSet of the carrier of S \ the carrier of J +* X) = (dom the non-empty ManySortedSet of the carrier of S \ the carrier of J) \/ (dom X) by FUNCT_4:def 1
.= ( the carrier of S \ the carrier of J) \/ (dom X) by PARTFUN1:def 2
.= ( the carrier of S \ the carrier of J) \/ I by PARTFUN1:def 2
.= the carrier of S \ the carrier of J by A1, XBOOLE_1:12 ;
then reconsider Y = the non-empty ManySortedSet of the carrier of S \ the carrier of J +* X as non-empty ManySortedSet of the carrier of S \ the carrier of J by RELAT_1:def 18, PARTFUN1:def 2;
consider Q being MSAlgebra over S such that
A2: ( Q is T -extension & the Sorts of Q | ( the carrier of S \ the carrier of J) = Y ) by Th17;

now :: thesis: for x being object st x in the carrier of S holds
not the Sorts of Q . x is empty

let x be object ; :: thesis: ( x in the carrier of S implies not the Sorts of Q . b₁ is empty )
assume x in the carrier of S ; :: thesis: not the Sorts of Q . b₁ is empty

per cases then ( x in the carrier of J or x in the carrier of S \ the carrier of J ) by XBOOLE_0:def 5;

suppose A3: x in the carrier of J ; :: thesis: not the Sorts of Q . b₁ is empty

then the Sorts of Q . x = the Sorts of T . x by A2, Th16;
hence not the Sorts of Q . x is empty by A3; :: thesis: verum

end;

suppose A4: x in the carrier of S \ the carrier of J ; :: thesis: not the Sorts of Q . b₁ is empty

then the Sorts of Q . x = Y . x by A2, FUNCT_1:49;
hence not the Sorts of Q . x is empty by A4; :: thesis: verum

end;

end;

end;

then the Sorts of Q is non-empty ;
then reconsider Q = Q as non-empty MSAlgebra over S by MSUALG_1:def 3;
take Q ; :: thesis: ( Q is T -extension & the Sorts of Q | I = X )
thus Q is T -extension by A2; :: thesis: the Sorts of Q | I = X
A5: dom X = I by PARTFUN1:def 2;
thus the Sorts of Q | I = ( the Sorts of Q | ( the carrier of S \ the carrier of J)) | I by A1, RELAT_1:74
.= X by A2, A5 ; :: thesis: verum