for J being non void Signature
for T being MSAlgebra over J
for X being ManySortedSubset of the Sorts of T
for S being non void b₁ -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X