theorem :: UNIALG_2:5

for U1 being Universal_Algebra
for A being non empty Subset of U1
for o being operation of U1 st A is_closed_on o holds
arity (o /. A) = arity o