let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for s being SortSymbol of S holds id (the Sorts of A . s) is Translation of A,s,s
let A be non-empty MSAlgebra of S; :: thesis: for s being SortSymbol of S holds id (the Sorts of A . s) is Translation of A,s,s
let s be SortSymbol of S; :: thesis: id (the Sorts of A . s) is Translation of A,s,s
thus TranslationRel S reduces s,s by REWRITE1:13; :: according to MSUALG_6:def 6 :: thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( id (the Sorts of A . s) = compose p,(the Sorts of A . s) & len q = (len p) + 1 & s = q . 1 & s = 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 ) )
A1: id (the Sorts of A . s) = compose {} ,(the Sorts of A . s) by FUNCT_7:41;
A2: <*s*> is RedSequence of TranslationRel S by REWRITE1:7;
A3: ( len <*s*> = 0 + 1 & len {} = 0 & <*s*> . 1 = s ) by FINSEQ_1:57;
for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom {} & f = {} . i & s1 = <*s*> . i & s2 = <*s*> . (i + 1) holds
f is_e.translation_of A,s1,s2 ;
hence ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( id (the Sorts of A . s) = compose p,(the Sorts of A . s) & len q = (len p) + 1 & s = q . 1 & s = 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 ) ) by A1, A2, A3; :: thesis: verum