theorem :: MSAFREE4:37

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms holds
B is X,S -terms ;