let X, Y be non empty set ; for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S1,S2 st F is uncurrying holds
F is monotone
let T be non empty Poset; for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S1,S2 st F is uncurrying holds
F is monotone
let S1 be non empty full SubRelStr of (T |^ Y) |^ X; for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S1,S2 st F is uncurrying holds
F is monotone
let S2 be non empty full SubRelStr of T |^ [:X,Y:]; for F being Function of S1,S2 st F is uncurrying holds
F is monotone
let F be Function of S1,S2; ( F is uncurrying implies F is monotone )
assume that
for x being set st x in dom F holds
x is Function-yielding Function
and
A1:
for f being Function st f in dom F holds
F . f = uncurry f
; WAYBEL27:def 1 F is monotone
let f, g be Element of S1; WAYBEL_1:def 2 ( not f <= g or F . f <= F . g )
reconsider a = f, b = g as Element of ((T |^ Y) |^ X) by YELLOW_0:58;
A2:
dom F = the carrier of S1
by FUNCT_2:def 1;
then A3:
F . g = uncurry b
by A1;
reconsider Fa = F . f, Fb = F . g as Element of (T |^ [:X,Y:]) by YELLOW_0:58;
assume
f <= g
; F . f <= F . g
then A4:
a <= b
by YELLOW_0:59;
A5:
the carrier of (T |^ Y) = Funcs (Y, the carrier of T)
by YELLOW_1:28;
then A6:
the carrier of ((T |^ Y) |^ X) = Funcs (X,(Funcs (Y, the carrier of T)))
by YELLOW_1:28;
A7:
F . f = uncurry a
by A2, A1;
now for xy being Element of [:X,Y:] holds Fa . xy <= Fb . xylet xy be
Element of
[:X,Y:];
Fa . xy <= Fb . xyconsider x,
y being
object such that A8:
x in X
and A9:
y in Y
and A10:
xy = [x,y]
by ZFMISC_1:def 2;
reconsider y =
y as
Element of
Y by A9;
reconsider x =
x as
Element of
X by A8;
A11:
a . x <= b . x
by A4, Th14;
b is
Function of
X,
(Funcs (Y, the carrier of T))
by A6, FUNCT_2:66;
then A12:
dom b = X
by FUNCT_2:def 1;
a is
Function of
X,
(Funcs (Y, the carrier of T))
by A6, FUNCT_2:66;
then A13:
dom a = X
by FUNCT_2:def 1;
b . x is
Function of
Y, the
carrier of
T
by A5, FUNCT_2:66;
then
dom (b . x) = Y
by FUNCT_2:def 1;
then A14:
Fb . (
x,
y)
= (b . x) . y
by A12, A3, FUNCT_5:38;
a . x is
Function of
Y, the
carrier of
T
by A5, FUNCT_2:66;
then
dom (a . x) = Y
by FUNCT_2:def 1;
then
Fa . (
x,
y)
= (a . x) . y
by A13, A7, FUNCT_5:38;
hence
Fa . xy <= Fb . xy
by A14, A11, A10, Th14;
verum end;
then
Fa <= Fb
by Th14;
hence
F . f <= F . g
by YELLOW_0:60; verum