let X be non empty set ; :: thesis: for S, T being non empty Poset
for f being Function of X,the carrier of (UPS S,T) holds commute f is directed-sups-preserving Function of S,(T |^ X)
let S, T be non empty Poset; :: thesis: for f being Function of X,the carrier of (UPS S,T) holds commute f is directed-sups-preserving Function of S,(T |^ X)
let f be Function of X,the carrier of (UPS S,T); :: thesis: commute f is directed-sups-preserving Function of S,(T |^ X)
A1: the carrier of (T |^ X) = Funcs X,the carrier of T by YELLOW_1:28;
A2: f in Funcs X,the carrier of (UPS S,T) by FUNCT_2:11;
A3: Funcs X,the carrier of (UPS S,T) c= Funcs X,(Funcs the carrier of S,the carrier of T) by Th22, FUNCT_5:63;
then commute f in Funcs the carrier of S,(Funcs X,the carrier of T) by A2, FUNCT_6:85;
then reconsider g = commute f as Function of S,(T |^ X) by A1, FUNCT_2:121;
A4: rng g c= Funcs X,the carrier of T by A1;
g is directed-sups-preserving

proof

let A be Subset of S; :: 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 S ;
A5: T |^ X = product (X --> T) by YELLOW_1:def 5;
then A6: dom (g . (sup A)) = X by WAYBEL_3:27;
assume A7: ex_sup_of A,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: A,T |^ X & "\/" (g .: A),(T |^ X) = g . ("\/" A,S) )

now

let x be Element of X; :: thesis: ex_sup_of pi (g .: A),x,(X --> T) . x
reconsider fx = f . x as directed-sups-preserving Function of S,T by Def4;
A8: fx preserves_sup_of B by WAYBEL_0:def 37;
commute g = f by A3, A2, FUNCT_6:87;
then A9: fx .: A = pi (g .: A),x by A4, Th8;
(X --> T) . x = T by FUNCOP_1:13;
hence ex_sup_of pi (g .: A),x,(X --> T) . x by A9, A8, A7, WAYBEL_0:def 31; :: thesis: verum

end;

hence A10: ex_sup_of g .: A,T |^ X by A5, YELLOW16:33; :: thesis: "\/" (g .: A),(T |^ X) = g . ("\/" A,S)

A11: now

let x be set ; :: thesis: ( x in X implies (sup (g .: A)) . x = (g . (sup A)) . x )
assume x in X ; :: thesis: (sup (g .: A)) . x = (g . (sup A)) . x
then reconsider a = x as Element of X ;
reconsider fx = f . a as directed-sups-preserving Function of S,T by Def4;
A12: (X --> T) . a = T by FUNCOP_1:13;
commute g = f by A3, A2, FUNCT_6:87;
then A13: fx .: A = pi (g .: A),a by A4, Th8;
fx preserves_sup_of B by WAYBEL_0:def 37;
then sup (pi (g .: B),a) = fx . (sup A) by A13, A7, WAYBEL_0:def 31;
then fx . (sup A) = (sup (g .: B)) . a by A5, A10, A12, YELLOW16:35;
hence (sup (g .: A)) . x = (g . (sup A)) . x by A3, A2, FUNCT_6:86; :: thesis: verum

end;

dom (sup (g .: A)) = X by A5, WAYBEL_3:27;
hence "\/" (g .: A),(T |^ X) = g . ("\/" A,S) by A11, A6, FUNCT_1:9; :: thesis: verum

end;

hence commute f is directed-sups-preserving Function of S,(T |^ X) ; :: thesis: verum