theorem Th25: :: AOFA_A01:25

for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for s being SortSymbol of S
for a being Element of A,s
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>