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 26 :: 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 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); :: 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) ;
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; :: thesis: verum