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 A1, XBOOLE_1:12 ;

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 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;

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

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 A1, XBOOLE_1:12 ;

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 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

then
the Sorts of Q is V2()
;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_{1} is empty )

assume x in the carrier of S ; :: thesis: not the Sorts of Q . b_{1} is empty

end;assume x in the carrier of S ; :: thesis: not the Sorts of Q . b

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;

end;

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