for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A, B being MSAlgebra over S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds
for x2 being Element of Args (o2,A)
for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2