let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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:12; :: 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: <*s*> is RedSequence of TranslationRel S by REWRITE1:6;
A2: len <*s*> = 0 + 1 by FINSEQ_1:40;
A3: len {} = 0 ;
A4: 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 ;
A5: <*s*> . 1 = s by FINSEQ_1:40;
id ( the Sorts of A . s) = compose ({},( the Sorts of A . s)) by FUNCT_7:39;
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, A5, A4; :: thesis: verum