let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being stable ManySortedRelation of A holds EqCl (R,A) is stable
let A be non-empty MSAlgebra over S; :: thesis: for R being stable ManySortedRelation of A holds EqCl (R,A) is stable
let R be stable ManySortedRelation of A; :: thesis: EqCl (R,A) is stable
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 (EqCl (R,A)) . s holds
[((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s
let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in (EqCl (R,A)) . s holds
[((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s
let a, b be set ; :: thesis: ( [a,b] in (EqCl (R,A)) . s implies [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s )
assume A1: [a,b] in (EqCl (R,A)) . s ; :: thesis: [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s
then reconsider a = a, b = b as Element of A,s by ZFMISC_1:87;
a,b are_convertible_wrt R . s by A1, Th42;
then (h . s) . a,(h . s) . b are_convertible_wrt R . s by Th45;
hence [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s by Th42; :: thesis: verum