let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let A be non-empty MSAlgebra of S; :: thesis: for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let R be ManySortedRelation of the Sorts of A; :: thesis: for s being SortSymbol of
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let s be SortSymbol of ; :: thesis: for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let a, b be Element of A,s; :: thesis: ( [a,b] in (TRS R) . s iff ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
A1: InvCl (StabCl R) = TRS R by Th37;

hereby :: thesis: ( ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) implies [a,b] in (TRS R) . s )

assume [a,b] in (TRS R) . s ; :: thesis: ex s' being SortSymbol of st
( TranslationRel S reduces s',s & ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) )
then consider s' being SortSymbol of , x, y being Element of A,s', t being Translation of A,s',s such that
A2: TranslationRel S reduces s',s and
A3: [x,y] in (StabCl R) . s' and
A4: a = t . x and
A5: b = t . y by A1, Th29;
take s' = s'; :: thesis: ( TranslationRel S reduces s',s & ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) )
thus TranslationRel S reduces s',s by A2; :: thesis: ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
reconsider t = t as Translation of A,s',s ;
consider u, v being Element of A,s', h being Endomorphism of A such that
A6: [u,v] in R . s' and
A7: x = (h . s') . u and
A8: y = (h . s') . v by A3, Th31;
take u = u; :: thesis: ex v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
take v = v; :: thesis: ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
take h = h; :: thesis: ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
take t = t; :: thesis: ( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
thus ( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) by A4, A5, A6, A7, A8; :: thesis: verum

end;

given s' being SortSymbol of such that A9: TranslationRel S reduces s',s and
A10: ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ; :: thesis: [a,b] in (TRS R) . s
consider l, r being Element of A,s', h being Endomorphism of A, t being Translation of A,s',s such that
A11: [l,r] in R . s' and
A12: a = t . ((h . s') . l) and
A13: b = t . ((h . s') . r) by A10;
[((h . s') . l),((h . s') . r)] in (StabCl R) . s' by A11, Th31;
hence [a,b] in (TRS R) . s by A1, A9, A12, A13, Th29; :: thesis: verum