let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant
let A be non-empty MSAlgebra over S; for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant
let R be invariant ManySortedRelation of A; EqCl (R,A) is invariant
let s1, s2 be SortSymbol of S; MSUALG_6:def 8 for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds
[(t . a),(t . b)] in (EqCl (R,A)) . s2
let t be Function; ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds
[(t . a),(t . b)] in (EqCl (R,A)) . s2 )
assume A1:
t is_e.translation_of A,s1,s2
; for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds
[(t . a),(t . b)] in (EqCl (R,A)) . s2
then reconsider t = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11;
let a, b be set ; ( [a,b] in (EqCl (R,A)) . s1 implies [(t . a),(t . b)] in (EqCl (R,A)) . s2 )
assume A2:
[a,b] in (EqCl (R,A)) . s1
; [(t . a),(t . b)] in (EqCl (R,A)) . s2
then reconsider a = a, b = b as Element of A,s1 by ZFMISC_1:87;
a,b are_convertible_wrt R . s1
by A2, Th42;
then
t . a,t . b are_convertible_wrt R . s2
by A1, Th47;
hence
[(t . a),(t . b)] in (EqCl (R,A)) . s2
by Th42; verum