let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )
let R be ManySortedRelation of the Sorts of A; :: thesis: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )
let s be SortSymbol of S; :: thesis: for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )
let a, b be Element of A,s; :: thesis: ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )
A1: InvCl (StabCl R) = TRS R by Th37;
hereby :: thesis: ( ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) implies [a,b] in (TRS R) . s )
assume [a,b] in (TRS R) . s ; :: thesis: ex s9 being SortSymbol of S st
( TranslationRel S reduces s9,s & ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) )
then consider s9 being SortSymbol of S, x, y being Element of A,s9, t being Translation of A,s9,s such that
A2: TranslationRel S reduces s9,s and
A3: [x,y] in (StabCl R) . s9 and
A4: a = t . x and
A5: b = t . y by A1, Th29;
take s9 = s9; :: thesis: ( TranslationRel S reduces s9,s & ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) )
thus TranslationRel S reduces s9,s by A2; :: thesis: ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) )
reconsider t = t as Translation of A,s9,s ;
consider u, v being Element of A,s9, h being Endomorphism of A such that
A6: [u,v] in R . s9 and
A7: x = (h . s9) . u and
A8: y = (h . s9) . v by A3, Th31;
take u = u; :: thesis: ex v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) )
take v = v; :: thesis: ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) )
take h = h; :: thesis: ex t being Translation of A,s9,s st
( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) )
take t = t; :: thesis: ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) )
thus ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) by A4, A5, A6, A7, A8; :: thesis: verum
end;
given s9 being SortSymbol of S such that A9: TranslationRel S reduces s9,s and
A10: ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st
( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ; :: thesis: [a,b] in (TRS R) . s
consider l, r being Element of A,s9, h being Endomorphism of A, t being Translation of A,s9,s such that
A11: [l,r] in R . s9 and
A12: a = t . ((h . s9) . l) and
A13: b = t . ((h . s9) . r) by A10;
[((h . s9) . l),((h . s9) . r)] in (StabCl R) . s9 by A11, Th31;
hence [a,b] in (TRS R) . s by A1, A9, A12, A13, Th29; :: thesis: verum