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
for Q being b₂ -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q