set I = the carrier of S \ the carrier of J;

set Z = the V2() ManySortedSet of the carrier of S \ the carrier of J;

consider Q being MSAlgebra over S such that

A1: ( Q is T -extension & the Sorts of Q | ( the carrier of S \ the carrier of J) = the V2() ManySortedSet of the carrier of S \ the carrier of J ) by Th17;

then reconsider Q = Q as non-empty MSAlgebra over S by MSUALG_1:def 3;

take Q ; :: thesis: Q is T -extension

thus Q is T -extension by A1; :: thesis: verum

set Z = the V2() ManySortedSet of the carrier of S \ the carrier of J;

consider Q being MSAlgebra over S such that

A1: ( Q is T -extension & the Sorts of Q | ( the carrier of S \ the carrier of J) = the V2() ManySortedSet of the carrier of S \ the carrier of J ) by Th17;

now :: thesis: for s being object st s in the carrier of S holds

not the Sorts of Q . s is empty

then
the Sorts of Q is V2()
;not the Sorts of Q . s is empty

let s be object ; :: thesis: ( s in the carrier of S implies not the Sorts of Q . b_{1} is empty )

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

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

per cases then
( s in the carrier of J or s 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

thus Q is T -extension by A1; :: thesis: verum