theorem Th14: :: MSUALG_6:14

for S being non empty non void ManySortedSign
for A being feasible MSAlgebra over S
for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) holds
( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )