theorem Th3: :: MSINST_1:3

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds
Args (o,U2) <> {}