let M be non empty set ; :: thesis: for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ M)
for i being Element of M holds (commute f) . i is directed-sups-preserving Function of S,T
let X, Y be non empty Poset; :: thesis: for f being directed-sups-preserving Function of X,(Y |^ M)
for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y
let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis: for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y
let i be Element of M; :: thesis: (commute f) . i is directed-sups-preserving Function of X,Y
A1: f in Funcs the carrier of X,(Funcs M,the carrier of Y) by Lm1;
then f is Function of the carrier of X,(Funcs M,the carrier of Y) by FUNCT_2:121;
then A2: rng f c= Funcs M,the carrier of Y by RELAT_1:def 19;
A3: rng (commute f) c= Funcs the carrier of X,the carrier of Y by Lm1;
dom (commute f) = M by Lm1;
then (commute f) . i in rng (commute f) by FUNCT_1:def 5;
then consider g being Function such that
A4: ( (commute f) . i = g & dom g = the carrier of X & rng g c= the carrier of Y ) by A3, FUNCT_2:def 2;
reconsider g = g as Function of X,Y by A4, FUNCT_2:4;
A5: Y |^ M = product (M --> Y) by YELLOW_1:def 5;
A6: (M --> Y) . i = Y by FUNCOP_1:13;
g is directed-sups-preserving

proof

let A be Subset of X; :: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or g preserves_sup_of A )
assume ( not A is empty & A is directed ) ; :: thesis: g preserves_sup_of A
then reconsider B = A as non empty directed Subset of X ;
A7: f preserves_sup_of B by WAYBEL_0:def 37;
assume ex_sup_of A,X ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: A,Y & "\/" (g .: A),Y = g . ("\/" A,X) )
then ( ex_sup_of f .: B,Y |^ M & sup (f .: B) = f . (sup B) ) by A7, WAYBEL_0:def 31;
then A8: ( ex_sup_of pi (f .: A),i,Y & sup (pi (f .: A),i) = (f . (sup A)) . i ) by A5, A6, YELLOW16:33, YELLOW16:35;
A9: pi (f .: A),i = g .: A by A2, A4, Th8;
thus ex_sup_of g .: A,Y by A2, A4, A8, Th8; :: thesis: "\/" (g .: A),Y = g . ("\/" A,X)
thus "\/" (g .: A),Y = g . ("\/" A,X) by A1, A4, A8, A9, FUNCT_6:86; :: thesis: verum

end;

hence (commute f) . i is directed-sups-preserving Function of X,Y by A4; :: thesis: verum