begin
begin
definition
let X be
set ;
existence
ex b1 being strict Lattice st
( the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
end;
begin
begin
definition
let I be non
empty set ;
let M be
ManySortedSet of
I;
existence
ex b1 being strict Lattice st
( ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
uniqueness
for b1, b2 being strict Lattice st ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & ( for x being set holds
( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
end;
begin
theorem Th13:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
o being
OperSymbol of
S for
C1,
C2 being
MSCongruence of
A for
C being
MSEquivalence-like ManySortedRelation of
A st
C = C1 "\/" C2 holds
for
x1,
y1 being
set for
n being
Element of
NAT for
a1,
a2,
b1 being
FinSequence st
len a1 = n &
len a1 = len a2 & ( for
k being
Element of
NAT st
k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) &
[((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) &
[x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for
x being
Element of
Args (
o,
A) st
x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)