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: (M --> Y) . i = Y ;
dom (commute f) = M by Lm1;
then A2: (commute f) . i in rng (commute f) by FUNCT_1:def 3;
A3: 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:66;
then A4: rng f c= Funcs (M, the carrier of Y) by RELAT_1:def 19;
rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) by Lm1;
then consider g being Function such that
A5: (commute f) . i = g and
A6: dom g = the carrier of X and
A7: rng g c= the carrier of Y by A2, FUNCT_2:def 2;
reconsider g = g as Function of X,Y by A6, A7, FUNCT_2:2;
A8: Y |^ M = product (M --> Y) by YELLOW_1:def 5;
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 ;
assume A9: ex_sup_of A,X ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: A,Y & "\/" ((g .: A),Y) = g . ("\/" (A,X)) )
A10: f preserves_sup_of B by WAYBEL_0:def 37;
then A11: ex_sup_of f .: B,Y |^ M by A9;
then ex_sup_of pi ((f .: A),i),Y by A8, A1, YELLOW16:31;
hence ex_sup_of g .: A,Y by A4, A5, Th8; :: thesis: "\/" ((g .: A),Y) = g . ("\/" (A,X))
A12: pi ((f .: A),i) = g .: A by A4, A5, Th8;
sup (f .: B) = f . (sup B) by A9, A10;
then sup (pi ((f .: A),i)) = (f . (sup A)) . i by A11, A8, A1, YELLOW16:33;
hence "\/" ((g .: A),Y) = g . ("\/" (A,X)) by A3, A5, A12, FUNCT_6:56; :: thesis: verum

end;

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