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 )
reconsider a = f, b = g as Element of ((T |^ X) |^ Y) by YELLOW_0:59;
reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) 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 |^ 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 ;
dom F = the carrier of S1 by FUNCT_2:def 1;
then A4: ( F . f = commute a & F . g = commute g ) by A1;

now

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

now

let y be Element of Y; :: thesis: (Fa . x) . y <= (Fb . x) . y
A5: a . y <= b . y by A2, Th14;
( (Fa . x) . y = (a . y) . x & (Fb . x) . y = (b . y) . x ) by A3, A4, FUNCT_6:86;
hence (Fa . x) . y <= (Fb . x) . y by A5, Th14; :: thesis: verum

end;

hence Fa . x <= Fb . x by 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