let S be locally_directed OrderSortedSign; :: thesis: 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; :: thesis: 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; :: thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies MSCng F is OSCongruence of U1 )
assume A1:
( F is_homomorphism U1,U2 & F is order-sorted )
; :: thesis: MSCng F is OSCongruence of U1
reconsider S1 = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
MSCng F is os-compatible
proof
let s1,
s2 be
Element of
S;
:: according to OSALG_4:def 1 :: thesis: ( 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 A2:
s1 <= s2
;
:: thesis: 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 ;
:: thesis: ( 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 A3:
(
x in the
Sorts of
U1 . s1 &
y in the
Sorts of
U1 . s1 )
;
:: thesis: ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 )
A4:
S1 . s3 c= S1 . s4
by A2, OSALG_1:def 18;
A5:
(
dom (F . s3) = S1 . s3 &
dom (F . s4) = S1 . s4 )
by FUNCT_2:def 1;
reconsider x1 =
x,
y1 =
y as
Element of the
Sorts of
U1 . s1 by A3;
reconsider x2 =
x,
y2 =
y as
Element of the
Sorts of
U1 . s2 by A3, A4;
A6:
(
[x2,y2] in MSCng F,
s2 iff
(F . s2) . x2 = (F . s2) . y2 )
by MSUALG_4:def 19;
A7:
(
x1 in dom (F . s4) &
(F . s3) . x1 = (F . s4) . x1 &
y1 in dom (F . s4) &
(F . s3) . y1 = (F . s4) . y1 )
by A1, A2, A5, OSALG_3:def 1;
(
(MSCng F) . s1 = MSCng F,
s1 &
(MSCng F) . s2 = MSCng F,
s2 )
by A1, MSUALG_4:def 20;
hence
(
[x,y] in (MSCng F) . s1 iff
[x,y] in (MSCng F) . s2 )
by A6, A7, MSUALG_4:def 19;
:: thesis: verum
end;
hence
MSCng F is OSCongruence of U1
by Def3; :: thesis: verum