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