let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant
let R be invariant ManySortedRelation of A; :: thesis: EqCl (R,A) 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 (EqCl (R,A)) . s1 holds
[(t . a),(t . b)] in (EqCl (R,A)) . s2
let t be Function; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: [(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; :: thesis: verum