let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A holds InvCl R is stable
let A be non-empty MSAlgebra over S; :: thesis: for R being stable ManySortedRelation of A holds InvCl R is stable
let R be stable ManySortedRelation of A; :: thesis: InvCl R is stable
let h be Endomorphism of A; :: according to MSUALG_6:def 9 :: thesis: for s being SortSymbol of S
for a, b being set st [a,b] in (InvCl R) . s holds
[((h . s) . a),((h . s) . b)] in (InvCl R) . s
let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in (InvCl R) . s holds
[((h . s) . a),((h . s) . b)] in (InvCl R) . s
let a, b be set ; :: thesis: ( [a,b] in (InvCl R) . s implies [((h . s) . a),((h . s) . b)] in (InvCl R) . s )
assume A1: [a,b] in (InvCl R) . s ; :: thesis: [((h . s) . a),((h . s) . b)] in (InvCl R) . s
then A2: b in the Sorts of A . s by ZFMISC_1:87;
a in the Sorts of A . s by A1, ZFMISC_1:87;
then consider s9 being SortSymbol of S, x, y being Element of A,s9, t being Translation of A,s9,s such that
A3: TranslationRel S reduces s9,s and
A4: [x,y] in R . s9 and
A5: a = t . x and
A6: b = t . y by A1, A2, Th29;
consider T being Translation of A,s9,s such that
A7: T * (h . s9) = (h . s) * t by A3, Th26;
(T * (h . s9)) . y = T . ((h . s9) . y) by FUNCT_2:15;
then A8: T . ((h . s9) . y) = (h . s) . b by A6, A7, FUNCT_2:15;
(T * (h . s9)) . x = T . ((h . s9) . x) by FUNCT_2:15;
then A9: T . ((h . s9) . x) = (h . s) . a by A5, A7, FUNCT_2:15;
[((h . s9) . x),((h . s9) . y)] in R . s9 by A4, Def9;
hence [((h . s) . a),((h . s) . b)] in (InvCl R) . s by A3, A9, A8, Th29; :: thesis: verum