let S1 be OrderSortedSign; for U1 being non-empty monotone OSAlgebra of S1
for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U1 be non-empty monotone OSAlgebra of S1; for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U2 be non-empty OSAlgebra of S1; for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let F be ManySortedFunction of U1,U2; ( F is order-sorted & F is_homomorphism U1,U2 implies ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 ) )
assume that
A1:
F is order-sorted
and
A2:
F is_homomorphism U1,U2
; ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;
F .:.: O1 is OrderSortedSet of S1
by A1, Th7;
then A3:
the Sorts of (Image F) is OrderSortedSet of S1
by A2, MSUALG_3:def 12;
then reconsider I = Image F as non-empty OSAlgebra of S1 by OSALG_1:17;
thus
Image F is order-sorted
by A3, OSALG_1:17; Image F is monotone OSAlgebra of S1
consider G being ManySortedFunction of U1,I such that
A4:
F = G
and
A5:
G is_epimorphism U1,I
by A2, MSUALG_3:21;
A6:
G is_homomorphism U1,I
by A5, MSUALG_3:def 8;
A7:
G is "onto"
by A5, MSUALG_3:def 8;
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
Den (o1,I) c= Den (o2,I)
proof
let o1,
o2 be
OperSymbol of
S1;
( o1 <= o2 implies Den (o1,I) c= Den (o2,I) )
assume A8:
o1 <= o2
;
Den (o1,I) c= Den (o2,I)
A9:
Args (
o1,
I)
c= Args (
o2,
I)
by A8, OSALG_1:26;
A10:
Args (
o1,
U1)
c= Args (
o2,
U1)
by A8, OSALG_1:26;
A11:
dom (Den (o2,I)) = Args (
o2,
I)
by FUNCT_2:def 1;
A12:
(Den (o2,U1)) | (Args (o1,U1)) = Den (
o1,
U1)
by A8, OSALG_1:def 21;
A13:
the_result_sort_of o1 <= the_result_sort_of o2
by A8;
for
a,
b being
object st
[a,b] in Den (
o1,
I) holds
[a,b] in Den (
o2,
I)
proof
set s1 =
the_result_sort_of o1;
set s2 =
the_result_sort_of o2;
o1 in the
carrier' of
S1
;
then A14:
o1 in dom the
ResultSort of
S1
by FUNCT_2:def 1;
let a,
b be
object ;
( [a,b] in Den (o1,I) implies [a,b] in Den (o2,I) )
assume A15:
[a,b] in Den (
o1,
I)
;
[a,b] in Den (o2,I)
A16:
a in Args (
o1,
I)
by A15, ZFMISC_1:87;
then consider y being
Element of
Args (
o1,
U1)
such that A17:
G # y = a
by A7, MSUALG_9:17;
reconsider y1 =
y as
Element of
Args (
o2,
U1)
by A10;
A18:
(
G # y1 = G # y &
(Den (o2,U1)) . y = (Den (o1,U1)) . y )
by A1, A4, A8, A12, Th12, FUNCT_1:49;
set x =
(Den (o1,U1)) . y;
(G . (the_result_sort_of o1)) . ((Den (o1,U1)) . y) = (Den (o1,I)) . a
by A6, A17, MSUALG_3:def 7;
then A19:
b = (G . (the_result_sort_of o1)) . ((Den (o1,U1)) . y)
by A15, FUNCT_1:1;
Result (
o1,
U1) =
(O1 * the ResultSort of S1) . o1
by MSUALG_1:def 5
.=
O1 . ( the ResultSort of S1 . o1)
by A14, FUNCT_1:13
.=
O1 . (the_result_sort_of o1)
by MSUALG_1:def 2
.=
dom (G . (the_result_sort_of o1))
by FUNCT_2:def 1
;
then
(G . (the_result_sort_of o1)) . ((Den (o1,U1)) . y) = (G . (the_result_sort_of o2)) . ((Den (o1,U1)) . y)
by A1, A4, A13;
then
b = (Den (o2,I)) . a
by A6, A17, A19, A18, MSUALG_3:def 7;
hence
[a,b] in Den (
o2,
I)
by A9, A11, A16, FUNCT_1:1;
verum
end;
hence
Den (
o1,
I)
c= Den (
o2,
I)
by RELAT_1:def 3;
verum
end;
hence
Image F is monotone OSAlgebra of S1
by OSALG_1:27; verum