theorem Th26: :: AOFA_A01:26

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