for J being non empty non void Signature
for S being b₁ -extension Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S st Q is T -extension holds
for x being object st x in the carrier of J holds
the Sorts of T . x = the Sorts of Q . x