theorem Th7: :: MSUALG_3:7

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x