let S be OrderSortedSign; for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone
let U1 be non-empty monotone OSAlgebra of S; for R being OSCongruence of U1 holds R is monotone
let R be OSCongruence of U1; R is monotone
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 R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume A1:
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 R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (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 R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
Args (o1,U1) c= Args (o2,U1)
by A1, OSALG_1:26;
then reconsider x3 = x1 as Element of Args (o2,U1) ;
let x2 be Element of Args (o2,U1); ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) )
assume
for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y)
; [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
then A2:
[((Den (o2,U1)) . x3),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
by MSUALG_4:def 4;
x1 in Args (o1,U1)
;
then A3:
x1 in dom (Den (o1,U1))
by FUNCT_2:def 1;
Den (o1,U1) c= Den (o2,U1)
by A1, OSALG_1:27;
hence
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2)
by A2, A3, GRFUNC_1:2; verum