let S be locally_directed OrderSortedSign; for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1
let U1, U2 be non-empty OSAlgebra of S; for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
MSCng F is OSCongruence of U1
let F be ManySortedFunction of U1,U2; ( F is_homomorphism U1,U2 & F is order-sorted implies MSCng F is OSCongruence of U1 )
assume that
A1:
F is_homomorphism U1,U2
and
A2:
F is order-sorted
; MSCng F is OSCongruence of U1
reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
MSCng F is os-compatible
proof
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 (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) )
assume A3:
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 (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 )
reconsider s3 =
s1,
s4 =
s2 as
SortSymbol 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 (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) )
assume A4:
(
x in the
Sorts of
U1 . s1 &
y in the
Sorts of
U1 . s1 )
;
( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 )
reconsider x1 =
x,
y1 =
y as
Element of the
Sorts of
U1 . s1 by A4;
S1 . s3 c= S1 . s4
by A3, OSALG_1:def 16;
then reconsider x2 =
x,
y2 =
y as
Element of the
Sorts of
U1 . s2 by A4;
A5:
(
[x2,y2] in MSCng (
F,
s2) iff
(F . s2) . x2 = (F . s2) . y2 )
by MSUALG_4:def 17;
dom (F . s3) = S1 . s3
by FUNCT_2:def 1;
then A6:
(
(F . s3) . x1 = (F . s4) . x1 &
(F . s3) . y1 = (F . s4) . y1 )
by A2, A3;
(MSCng F) . s1 = MSCng (
F,
s1)
by A1, MSUALG_4:def 18;
hence
(
[x,y] in (MSCng F) . s1 iff
[x,y] in (MSCng F) . s2 )
by A1, A5, A6, MSUALG_4:def 17, MSUALG_4:def 18;
verum
end;
hence
MSCng F is OSCongruence of U1
by Def2; verum