let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A holds InvCl R is stable
let A be non-empty MSAlgebra of 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:106;
a in the Sorts of A . s by A1, ZFMISC_1:106;
then consider s' being SortSymbol of S, x, y being Element of A,s', t being Translation of A,s',s such that
A3: TranslationRel S reduces s',s and
A4: [x,y] in R . s' and
A5: a = t . x and
A6: b = t . y by A1, A2, Th29;
consider T being Translation of A,s',s such that
A7: T * (h . s') = (h . s) * t by A3, Th26;
(T * (h . s')) . y = T . ((h . s') . y) by FUNCT_2:21;
then A8: T . ((h . s') . y) = (h . s) . b by A6, A7, FUNCT_2:21;
(T * (h . s')) . x = T . ((h . s') . x) by FUNCT_2:21;
then A9: T . ((h . s') . x) = (h . s) . a by A5, A7, FUNCT_2:21;
[((h . s') . x),((h . s') . y)] in R . s' by A4, Def9;
hence [((h . s) . a),((h . s) . b)] in (InvCl R) . s by A3, A9, A8, Th29; :: thesis: verum