theorem Th5: :: PRALG_2:5

for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]