reconsider R = id the carrier of S,the Sorts of A as ManySortedRelation of A ;
take
R
; :: thesis: ( R is invariant & R is stable & R is MSEquivalence-like )
thus
R is invariant
:: thesis: ( R is stable & R is MSEquivalence-like )proof
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
A1:
(
R . s1 = id (the Sorts of A . s1) &
R . s2 = id (the Sorts of A . s2) )
by Def10;
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 reconsider f =
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 R . s1 implies [(t . a),(t . b)] in R . s2 )
assume A2:
[a,b] in R . s1
;
:: thesis: [(t . a),(t . b)] in R . s2
then
a in the
Sorts of
A . s1
by ZFMISC_1:106;
then
(
a = b &
f . a in the
Sorts of
A . s2 )
by A1, A2, FUNCT_2:7, RELAT_1:def 10;
hence
[(t . a),(t . b)] in R . s2
by A1, RELAT_1:def 10;
:: thesis: verum
end;
thus
R is stable
:: thesis: R is MSEquivalence-like proof
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 R . s holds
[((h . s) . a),((h . s) . b)] in R . slet s be
SortSymbol of
S;
:: thesis: for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s
A3:
R . s = id (the Sorts of A . s)
by Def10;
let a,
b be
set ;
:: thesis: ( [a,b] in R . s implies [((h . s) . a),((h . s) . b)] in R . s )
assume
[a,b] in R . s
;
:: thesis: [((h . s) . a),((h . s) . b)] in R . s
then A4:
(
a = b &
a in the
Sorts of
A . s )
by A3, RELAT_1:def 10;
then
(h . s) . a in the
Sorts of
A . s
by FUNCT_2:7;
hence
[((h . s) . a),((h . s) . b)] in R . s
by A3, A4, RELAT_1:def 10;
:: thesis: verum
end;
let i be set ; :: according to MSUALG_4:def 3,MSUALG_4:def 5 :: thesis: for b1 being Element of bool [:(the Sorts of A . i),(the Sorts of A . i):] holds
( not i in the carrier of S or not R . i = b1 or b1 is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):] )
let P be Relation of (the Sorts of A . i); :: thesis: ( not i in the carrier of S or not R . i = P or P is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):] )
assume
i in the carrier of S
; :: thesis: ( not R . i = P or P is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):] )
then reconsider s = i as SortSymbol of S ;
assume
R . i = P
; :: thesis: P is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):]
then
P = id (the Sorts of A . s)
by Def10;
hence
P is Element of bool [:(the Sorts of A . i),(the Sorts of A . i):]
; :: thesis: verum