let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
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 Translation of A,s1,s2
let A be non-empty MSAlgebra over S; :: thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
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 Translation of A,s1,s2
let s1, s2 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 implies 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 Translation of A,s1,s2 )
assume A1: TranslationRel S reduces s1,s2 ; :: thesis: 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 Translation of A,s1,s2
let q be RedSequence of TranslationRel S; :: thesis: 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 Translation of A,s1,s2
let p be Function-yielding FinSequence; :: thesis: ( 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 ) implies compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 )
assume that
A2: len q = (len p) + 1 and
A3: s1 = q . 1 and
A4: s2 = q . (len q) and
A5: 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 ; :: thesis: compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2
compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A2, A3, A4, A5, Th14;
hence compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 by A1, A2, A3, A4, A5, Def6; :: thesis: verum