reconsider R = id ( the carrier of S, the Sorts of A) as ManySortedRelation of A ;
take R ; :: thesis: ( R is invariant & R is stable & R is MSEquivalence-like )
thus R is invariant :: thesis: ( R is stable & R is MSEquivalence-like )

proof

let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def 8 :: thesis: for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
let t be Function; :: thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 )
assume t is_e.translation_of A,s1,s2 ; :: thesis: for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
then reconsider f = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11;
let a, b be set ; :: thesis: ( [a,b] in R . s1 implies [(t . a),(t . b)] in R . s2 )
assume A1: [a,b] in R . s1 ; :: thesis: [(t . a),(t . b)] in R . s2
then a in the Sorts of A . s1 by ZFMISC_1:87;
then A2: f . a in the Sorts of A . s2 by FUNCT_2:5;
R . s1 = id ( the Sorts of A . s1) by Def10;
then A3: a = b by A1, RELAT_1:def 10;
R . s2 = id ( the Sorts of A . s2) by Def10;
hence [(t . a),(t . b)] in R . s2 by A3, A2, RELAT_1:def 10; :: thesis: verum

end;

thus R is stable :: thesis: R is MSEquivalence-like

proof

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 R . s holds
[((h . s) . a),((h . s) . b)] in R . s
let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s
let a, b be set ; :: thesis: ( [a,b] in R . s implies [((h . s) . a),((h . s) . b)] in R . s )
A4: R . s = id ( the Sorts of A . s) by Def10;
assume A5: [a,b] in R . s ; :: thesis: [((h . s) . a),((h . s) . b)] in R . s
then a in the Sorts of A . s by A4, RELAT_1:def 10;
then A6: (h . s) . a in the Sorts of A . s by FUNCT_2:5;
a = b by A4, A5, RELAT_1:def 10;
hence [((h . s) . a),((h . s) . b)] in R . s by A4, A6, RELAT_1:def 10; :: thesis: verum

end;

let i be object ; :: according to MSUALG_4:def 2,MSUALG_4:def 3 :: thesis: for b₁ being Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] holds
( not i in the carrier of S or not R . i = b₁ or b₁ is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
let P be Relation of ( the Sorts of A . i); :: thesis: ( not i in the carrier of S or not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
assume i in the carrier of S ; :: thesis: ( not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
then reconsider s = i as SortSymbol of S ;
assume R . i = P ; :: thesis: P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
then P = id ( the Sorts of A . s) by Def10;
hence P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ; :: thesis: verum