set Z = the ManySortedSet of {} ;

{} c= the carrier of S \ the carrier of J ;

then consider Q being MSAlgebra over S such that

A1: ( Q is T -extension & the Sorts of Q | {} = the ManySortedSet of {} ) by Th17;

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

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

{} c= the carrier of S \ the carrier of J ;

then consider Q being MSAlgebra over S such that

A1: ( Q is T -extension & the Sorts of Q | {} = the ManySortedSet of {} ) by Th17;

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

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