theorem Th22: :: PRALG_3:22

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)