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 V2() 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 V2() 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 V2() 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 V2() 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 V2() 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 V2() 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 V2() ManySortedSet of the carrier of S \ the carrier of J +* X;
dom ( the V2() ManySortedSet of the carrier of S \ the carrier of J +* X) = (dom the V2() 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 ;
then reconsider Y = the V2() ManySortedSet of the carrier of S \ the carrier of J +* X as V2() ManySortedSet of the carrier of S \ the carrier of J by ;
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 . b1 is empty )
assume x in the carrier of S ; :: thesis: not the Sorts of Q . b1 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 . b1 is empty
then the Sorts of Q . x = the Sorts of T . x by ;
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 . b1 is empty
then the Sorts of Q . x = Y . x by ;
hence not the Sorts of Q . x is empty by A4; :: thesis: verum
end;
end;
end;
then the Sorts of Q is V2() ;
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
.= X by A2, A5 ; :: thesis: verum