let S be locally_directed OrderSortedSign; for U1 being non-empty OSAlgebra of S
for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let U1 be non-empty OSAlgebra of S; for U2 being non-empty monotone OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let U2 be non-empty monotone OSAlgebra of S; for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
OSCng F is monotone
let F be ManySortedFunction of U1,U2; ( F is_homomorphism U1,U2 & F is order-sorted implies OSCng F is monotone )
assume that
A1:
F is_homomorphism U1,U2
and
A2:
F is order-sorted
; OSCng F is monotone
reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set O1 = the Sorts of U1;
let o1, o2 be OperSymbol of S; OSALG_4:def 26 ( o1 <= o2 implies for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) )
assume A3:
o1 <= o2
; for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
A4:
(Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2)
by A3, OSALG_1:def 21;
set R = OSCng F;
set rs1 = the_result_sort_of o1;
set rs2 = the_result_sort_of o2;
let x1 be Element of Args (o1,U1); for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
let x2 be Element of Args (o2,U1); ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) )
assume A5:
for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y)
; [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
Args (o1,U1) c= Args (o2,U1)
by A3, OSALG_1:26;
then reconsider x12 = x1 as Element of Args (o2,U1) ;
set D1 = (Den (o1,U1)) . x1;
set D2 = (Den (o2,U1)) . x2;
set M = MSCng F;
A6:
(Den (o1,U1)) . x1 in S1 . (the_result_sort_of o1)
by MSUALG_9:18;
F # x1 in Args (o1,U2)
;
then A7:
F # x1 in dom (Den (o1,U2))
by FUNCT_2:def 1;
A8:
the_result_sort_of o1 <= the_result_sort_of o2
by A3;
then
S1 . (the_result_sort_of o1) c= S1 . (the_result_sort_of o2)
by OSALG_1:def 16;
then reconsider D11 = (Den (o1,U1)) . x1, D12 = (Den (o2,U1)) . x12 as Element of the Sorts of U1 . (the_result_sort_of o2) by MSUALG_9:18;
(Den (o1,U1)) . x1 in dom (F . (the_result_sort_of o1))
by A6, FUNCT_2:def 1;
then (F . (the_result_sort_of o2)) . ((Den (o1,U1)) . x1) =
(F . (the_result_sort_of o1)) . ((Den (o1,U1)) . x1)
by A2, A8
.=
(Den (o1,U2)) . (F # x1)
by A1
.=
(Den (o2,U2)) . (F # x1)
by A7, A4, FUNCT_1:47
.=
(Den (o2,U2)) . (F # x12)
by A2, A3, OSALG_3:12
.=
(F . (the_result_sort_of o2)) . ((Den (o2,U1)) . x12)
by A1
;
then A9:
( (Den (o2,U1)) . x2 in the Sorts of U1 . (the_result_sort_of o2) & [D11,D12] in MSCng (F,(the_result_sort_of o2)) )
by MSUALG_4:def 17, MSUALG_9:18;
field ((OSCng F) . (the_result_sort_of o2)) = the Sorts of U1 . (the_result_sort_of o2)
by ORDERS_1:12;
then A10:
(OSCng F) . (the_result_sort_of o2) is_transitive_in the Sorts of U1 . (the_result_sort_of o2)
by RELAT_2:def 16;
A11:
[((Den (o2,U1)) . x12),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
by A5, MSUALG_4:def 4;
( (MSCng F) . (the_result_sort_of o2) = MSCng (F,(the_result_sort_of o2)) & MSCng F = OSCng F )
by A1, A2, Def23, MSUALG_4:def 18;
hence
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2)
by A11, A9, A10, RELAT_2:def 8; verum