let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
let R be ManySortedRelation of A; :: thesis: ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )

hereby :: thesis: ( ( for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies R is invariant )

defpred S₁[ Function, set , set ] means for a, b being set st [a,b] in R . $2 holds
[($1 . a),($1 . b)] in R . $3;
deffunc H₁( SortSymbol of S) -> Element of bool [:( the Sorts of A . $1),( the Sorts of A . $1):] = id ( the Sorts of A . $1);
assume A1: R is invariant ; :: thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 holds S₁[t,s1,s2]
A2: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A,s2,s3 holds
S₁[f * t,s1,s3]

proof

let s1, s2, s3 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A,s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A,s2,s3 holds
S₁[f * t,s1,s3] )
assume TranslationRel S reduces s1,s2 ; :: thesis: for t being Translation of A,s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of A,s2,s3 holds
S₁[f * t,s1,s3]
let t be Translation of A,s1,s2; :: thesis: ( S₁[t,s1,s2] implies for f being Function st f is_e.translation_of A,s2,s3 holds
S₁[f * t,s1,s3] )
assume A3: for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 ; :: thesis: for f being Function st f is_e.translation_of A,s2,s3 holds
S₁[f * t,s1,s3]
let f be Function; :: thesis: ( f is_e.translation_of A,s2,s3 implies S₁[f * t,s1,s3] )
assume A4: f is_e.translation_of A,s2,s3 ; :: thesis: S₁[f * t,s1,s3]
let a, b be set ; :: thesis: ( [a,b] in R . s1 implies [((f * t) . a),((f * t) . b)] in R . s3 )
assume A5: [a,b] in R . s1 ; :: thesis: [((f * t) . a),((f * t) . b)] in R . s3
then reconsider a9 = a, b9 = b as Element of A,s1 by ZFMISC_1:87;
[(t . a9),(t . b9)] in R . s2 by A3, A5;
then A6: [(f . (t . a9)),(f . (t . b9))] in R . s3 by A1, A4;
f . (t . a9) = (f * t) . a9 by FUNCT_2:15;
hence [((f * t) . a),((f * t) . b)] in R . s3 by A6, FUNCT_2:15; :: thesis: verum

end;

A7: for s being SortSymbol of S holds S₁[ id ( the Sorts of A . s),s,s]

proof

let s be SortSymbol of S; :: thesis: S₁[ id ( the Sorts of A . s),s,s]
let a, b be set ; :: thesis: ( [a,b] in R . s implies [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s )
assume A8: [a,b] in R . s ; :: thesis: [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s
then a in the Sorts of A . s by ZFMISC_1:87;
then A9: H₁(s) . a = a by FUNCT_1:17;
b in the Sorts of A . s by A8, ZFMISC_1:87;
hence [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s by A8, A9, FUNCT_1:17; :: thesis: verum

end;

thus for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 holds S₁[t,s1,s2] from MSUALG_6:sch 1(A7, A2); :: thesis: verum

end;

assume A10: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ; :: thesis: R is invariant
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 A11: 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 t is Translation of A,s1,s2 by Th17;
hence for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 by A10, A11, Th17; :: thesis: verum