let X, Y be non empty set ; :: thesis: for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ X) |^ Y
for S2 being non empty full SubRelStr of (T |^ Y) |^ X
for F being Function of S1,S2 st F is commuting holds
F is monotone
let T be non empty Poset; :: thesis: for S1 being non empty full SubRelStr of (T |^ X) |^ Y
for S2 being non empty full SubRelStr of (T |^ Y) |^ X
for F being Function of S1,S2 st F is commuting holds
F is monotone
let S1 be non empty full SubRelStr of (T |^ X) |^ Y; :: thesis: for S2 being non empty full SubRelStr of (T |^ Y) |^ X
for F being Function of S1,S2 st F is commuting holds
F is monotone
let S2 be non empty full SubRelStr of (T |^ Y) |^ X; :: thesis: for F being Function of S1,S2 st F is commuting holds
F is monotone
let F be Function of S1,S2; :: thesis: ( F is commuting 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 = commute f ; :: according to WAYBEL27:def 3 :: 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 )
A2: dom F = the carrier of S1 by FUNCT_2:def 1;
then A3: F . g = commute g by A1;
reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:58;
reconsider a = f, b = g as Element of ((T |^ X) |^ Y) by YELLOW_0:58;
A4: the carrier of ((T |^ X) |^ Y) = Funcs (Y, the carrier of (T |^ X)) by YELLOW_1:28
.= Funcs (Y,(Funcs (X, the carrier of T))) by YELLOW_1:28 ;
assume f <= g ; :: thesis: F . f <= F . g
then A5: a <= b by YELLOW_0:59;
A6: F . f = commute 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
A7: (Fa . x) . y = (a . y) . x by A4, A6, FUNCT_6:56;
A8: (Fb . x) . y = (b . y) . x by A4, A3, FUNCT_6:56;
a . y <= b . y by A5, Th14;
hence (Fa . x) . y <= (Fb . x) . y by A7, A8, 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