let S be locally_directed OrderSortedSign; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: according to OSALG_4:def 28 :: thesis: ( 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 ; :: thesis: 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 23;
set R = OSCng F;
set w1 = the_arity_of o1;
set w2 = the_arity_of o2;
set rs1 = the_result_sort_of o1;
set rs2 = the_result_sort_of o2;
let x1 be Element of Args o1,U1; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: [((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 by TARSKI:def 3;
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:19;
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, OSALG_1:def 22;
then S1 . (the_result_sort_of o1) c= S1 . (the_result_sort_of o2) by OSALG_1:def 18;
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 A6, MSUALG_9:19;
(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, OSALG_3:def 1
.= (Den o1,U2) . (F # x1) by A1, MSUALG_3:def 9
.= (Den o2,U2) . (F # x1) by A7, A4, FUNCT_1:70
.= (Den o2,U2) . (F # x12) by A2, A3, OSALG_3:13
.= (F . (the_result_sort_of o2)) . ((Den o2,U1) . x12) by A1, MSUALG_3:def 9 ;
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 19, MSUALG_9:19;
field ((OSCng F) . (the_result_sort_of o2)) = the Sorts of U1 . (the_result_sort_of o2) by ORDERS_1:97;
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 6;
( (MSCng F) . (the_result_sort_of o2) = MSCng F,(the_result_sort_of o2) & MSCng F = OSCng F ) by A1, A2, Def25, MSUALG_4:def 20;
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; :: thesis: verum