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 S2,S1 st F is currying 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 S2,S1 st F is currying 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 S2,S1 st F is currying holds
F is monotone
let S2 be non empty full SubRelStr of T |^ [:X,Y:]; :: thesis: for F being Function of S2,S1 st F is currying holds
F is monotone
let F be Function of S2,S1; :: thesis: ( F is currying implies F is monotone )
assume that
for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) and
A1: for f being Function st f in dom F holds
F . f = curry f ; :: according to WAYBEL27:def 2 :: thesis: F is monotone
let f, g be Element of S2; :: according to WAYBEL_1:def 2 :: thesis: ( not f <= g or F . f <= F . g )
reconsider a = f, b = g as Element of (T |^ [:X,Y:]) by YELLOW_0:58;
A2: dom F = the carrier of S2 by FUNCT_2:def 1;
then A3: F . g = curry b by A1;
reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:58;
assume f <= g ; :: thesis: 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 = curry a by A2, A1;

now :: thesis: for x being Element of X holds Fa . x <= Fb . x

let x be Element of X; :: thesis: Fa . x <= Fb . x

now :: thesis: for y being Element of Y holds (Fa . x) . y <= (Fb . x) . y

let y be Element of Y; :: thesis: (Fa . x) . y <= (Fb . x) . y
reconsider xy = [x,y] as Element of [:X,Y:] ;
Fa . x is Function of Y, the carrier of T by A5, FUNCT_2:66;
then A8: dom (Fa . x) = Y by FUNCT_2:def 1;
Fa is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66;
then dom Fa = X by FUNCT_2:def 1;
then (Fa . x) . y = a . (x,y) by A8, A7, FUNCT_5:31;
then A9: (Fa . x) . y = a . xy ;
Fb . x is Function of Y, the carrier of T by A5, FUNCT_2:66;
then A10: dom (Fb . x) = Y by FUNCT_2:def 1;
Fb is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66;
then dom Fb = X by FUNCT_2:def 1;
then (Fb . x) . y = b . (x,y) by A10, A3, FUNCT_5:31;
hence (Fa . x) . y <= (Fb . x) . y by A9, A4, Th14; :: thesis: verum

end;

hence Fa . x <= Fb . x by Th14; :: thesis: verum

end;

then Fa <= Fb by Th14;
hence F . f <= F . g by YELLOW_0:60; :: thesis: verum