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 A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ; :: thesis: OSCng F is monotone
set O1 = the Sorts of U1;
reconsider S1 = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
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 A2: 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)
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 A3: 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)
set D1 = (Den o1,U1) . x1;
set D2 = (Den o2,U1) . x2;
set M = MSCng F;
A4: ( (MSCng F) . (the_result_sort_of o1) = MSCng F,(the_result_sort_of o1) & (MSCng F) . (the_result_sort_of o2) = MSCng F,(the_result_sort_of o2) & MSCng F = OSCng F ) by A1, Def25, MSUALG_4:def 20;
A5: ( Args o1,U1 c= Args o2,U1 & Result o1,U1 c= Result o2,U1 ) by A2, OSALG_1:26;
A6: ( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by A2, OSALG_1:def 22;
then A7: S1 . (the_result_sort_of o1) c= S1 . (the_result_sort_of o2) by OSALG_1:def 18;
reconsider x12 = x1 as Element of Args o2,U1 by A5, TARSKI:def 3;
A8: [((Den o2,U1) . x12),((Den o2,U1) . x2)] in (OSCng F) . (the_result_sort_of o2) by A3, MSUALG_4:def 6;
A9: ( (Den o2,U1) . x2 in the Sorts of U1 . (the_result_sort_of o2) & (Den o2,U1) . x12 in the Sorts of U1 . (the_result_sort_of o2) & (Den o1,U1) . x1 in S1 . (the_result_sort_of o1) ) by MSUALG_9:19;
then A10: ( (Den o1,U1) . x1 in S1 . (the_result_sort_of o2) & (Den o1,U1) . x1 in dom (F . (the_result_sort_of o1)) ) by A7, FUNCT_2:def 1;
reconsider D11 = (Den o1,U1) . x1, D12 = (Den o2,U1) . x12 as Element of the Sorts of U1 . (the_result_sort_of o2) by A7, A9;
F # x1 in Args o1,U2 ;
then A11: F # x1 in dom (Den o1,U2) by FUNCT_2:def 1;
A12: (Den o2,U2) | (Args o1,U2) = Den o1,U2 by A2, OSALG_1:def 23;
(F . (the_result_sort_of o2)) . ((Den o1,U1) . x1) = (F . (the_result_sort_of o1)) . ((Den o1,U1) . x1) by A1, A6, A10, OSALG_3:def 1
.= (Den o1,U2) . (F # x1) by A1, MSUALG_3:def 9
.= (Den o2,U2) . (F # x1) by A11, A12, FUNCT_1:70
.= (Den o2,U2) . (F # x12) by A1, A2, OSALG_3:13
.= (F . (the_result_sort_of o2)) . ((Den o2,U1) . x12) by A1, MSUALG_3:def 9 ;
then A13: [D11,D12] in MSCng F,(the_result_sort_of o2) by MSUALG_4:def 19;
field ((OSCng F) . (the_result_sort_of o2)) = the Sorts of U1 . (the_result_sort_of o2) by ORDERS_1:97;
then (OSCng F) . (the_result_sort_of o2) is_transitive_in the Sorts of U1 . (the_result_sort_of o2) by RELAT_2:def 16;
hence [((Den o1,U1) . x1),((Den o2,U1) . x2)] in (OSCng F) . (the_result_sort_of o2) by A4, A8, A9, A13, RELAT_2:def 8; :: thesis: verum