scheme :: MSUALG_6:sch 1
TranslationInd{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set , set , set ] } :
for s1, s2 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds
for t being Translation of F2(),s1,s2 holds P1[t,s1,s2]
provided
A1: for s being SortSymbol of F1() holds P1[ id ( the Sorts of F2() . s),s,s] and
A2: for s1, s2, s3 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds
for t being Translation of F2(),s1,s2 st P1[t,s1,s2] holds
for f being Function st f is_e.translation_of F2(),s2,s3 holds
P1[f * t,s1,s3]