for J being non empty non void Signature
for S being b₁ -extension Signature
for T being MSAlgebra over J
for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension