let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 )

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]
deffunc H₁( SortSymbol of S) -> Element of bool [:(the Sorts of A . $1),(the Sorts of A . $1):] = id (the Sorts of A . $1);
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;
A2: 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 A3: [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 & b in the Sorts of A . s ) by ZFMISC_1:106;
then ( H₁(s) . a = a & H₁(s) . b = b ) by FUNCT_1:34;
hence [((id (the Sorts of A . s)) . a),((id (the Sorts of A . s)) . b)] in R . s by A3; :: thesis: verum

end;

A4: 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 A5: 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 A6: 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 A7: [a,b] in R . s1 ; :: thesis: [((f * t) . a),((f * t) . b)] in R . s3
then reconsider a' = a, b' = b as Element of A,s1 by ZFMISC_1:106;
[(t . a'),(t . b')] in R . s2 by A5, A7;
then A8: [(f . (t . a')),(f . (t . b'))] in R . s3 by A1, A6, Def8;
f . (t . a') = (f * t) . a' by FUNCT_2:21;
hence [((f * t) . a),((f * t) . b)] in R . s3 by A8, FUNCT_2:21; :: 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(A2, A4); :: thesis: verum

end;

assume A9: 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 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 ( TranslationRel S reduces s1,s2 & 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 A9; :: thesis: verum