let X, Y be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: for F being Function of S1,S2 st F is uncurrying holds
F is monotone
let F be Function of S1,S2; :: thesis: ( 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
; :: according to WAYBEL27:def 1 :: thesis: F is monotone
let f, g be Element of S1; :: according to WAYBEL_1:def 2 :: thesis: ( not f <= g or F . f <= F . g )
reconsider a = f, b = g as Element of ((T |^ Y) |^ X) by YELLOW_0:59;
reconsider Fa = F . f, Fb = F . g as Element of (T |^ [:X,Y:]) by YELLOW_0:59;
assume
f <= g
; :: thesis: F . f <= F . g
then A2:
a <= b
by YELLOW_0:60;
A3:
the carrier of (T |^ Y) = Funcs Y,the carrier of T
by YELLOW_1:28;
then A4:
the carrier of ((T |^ Y) |^ X) = Funcs X,(Funcs Y,the carrier of T)
by YELLOW_1:28;
dom F = the carrier of S1
by FUNCT_2:def 1;
then A5:
( F . f = uncurry a & F . g = uncurry b )
by A1;
now let xy be
Element of
[:X,Y:];
:: thesis: Fa . xy <= Fb . xyconsider x,
y being
set such that A6:
(
x in X &
y in Y &
xy = [x,y] )
by ZFMISC_1:def 2;
reconsider x =
x as
Element of
X by A6;
reconsider y =
y as
Element of
Y by A6;
(
a . x is
Function of
Y,the
carrier of
T &
b . x is
Function of
Y,the
carrier of
T &
a is
Function of
X,
(Funcs Y,the carrier of T) &
b is
Function of
X,
(Funcs Y,the carrier of T) )
by A3, A4, FUNCT_2:121;
then
(
dom (a . x) = Y &
dom (b . x) = Y &
x in X &
y in Y &
dom a = X &
dom b = X )
by FUNCT_2:def 1;
then
(
Fa . x,
y = (a . x) . y &
Fb . x,
y = (b . x) . y &
a . x <= b . x )
by A2, A5, Th14, FUNCT_5:45;
hence
Fa . xy <= Fb . xy
by A6, Th14;
:: thesis: verum end;
then
( Fa <= Fb & F . f in the carrier of S2 )
by Th14;
hence
F . f <= F . g
by YELLOW_0:61; :: thesis: verum