deffunc H1( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S);
consider f being Function such that
A1:
( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) )
from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def 1;
reconsider f = f as ManySortedRelation of U1 ;
for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
then
f is MSEquivalence_Relation-like
by MSUALG_4:def 2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def 3;
set f1 = f;
f is os-compatible
proof
reconsider X = the
Sorts of
U1 as
OrderSortedSet of
S by OSALG_1:17;
let s1,
s2 be
Element of
S;
OSALG_4:def 1 ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume A2:
s1 <= s2
;
for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds
( [x,y] in f . s1 iff [x,y] in f . s2 )
reconsider s3 =
s1,
s4 =
s2 as
Element of
S ;
let x,
y be
set ;
( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) )
assume that A3:
x in the
Sorts of
U1 . s1
and
y in the
Sorts of
U1 . s1
;
( [x,y] in f . s1 iff [x,y] in f . s2 )
A4:
f . s1 = id (X . s1)
by A1;
A5:
f . s2 = id (X . s2)
by A1;
X . s3 c= X . s4
by A2, OSALG_1:def 16;
then
id (X . s1) c= id (X . s2)
by SYSREL:15;
hence
(
[x,y] in f . s1 implies
[x,y] in f . s2 )
by A4, A5;
( [x,y] in f . s2 implies [x,y] in f . s1 )
assume
[x,y] in f . s2
;
[x,y] in f . s1
then
x = y
by A5, RELAT_1:def 10;
hence
[x,y] in f . s1
by A4, A3, RELAT_1:def 10;
verum
end;
then reconsider f = f as MSEquivalence-like OrderSortedRelation of U1 by Def2;
take
f
; f is MSCongruence-like
for o being Element of the carrier' of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
proof
let o be
Element of the
carrier' of
S;
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)let x,
y be
Element of
Args (
o,
U1);
( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) )
A6:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
assume A7:
for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n)
;
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
A8:
for
a being
object st
a in dom (the_arity_of o) holds
x . a = y . a
set r =
the_result_sort_of o;
A11:
f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o))
by A1;
A12:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
then A13:
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by PARTFUN1:def 2;
A14:
Result (
o,
U1) =
( the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . o)
by A12, A13, FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 2
;
dom y = dom (the_arity_of o)
by MSUALG_3:6;
then
(Den (o,U1)) . x = (Den (o,U1)) . y
by A6, A8, FUNCT_1:2;
hence
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
by A11, A14, RELAT_1:def 10;
verum
end;
hence
f is MSCongruence-like
by MSUALG_4:def 4; verum