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:8;
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:56;
then commute f in Funcs ( the carrier of S,(Funcs (X, the carrier of T))) by A2, FUNCT_6:55;
then reconsider g = commute f as Function of S,(T |^ X) by A1, FUNCT_2:66;
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 :: thesis: for x being Element of X holds ex_sup_of pi ((g .: A),x),(X --> T) . x

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:57;
then A9: fx .: A = pi ((g .: A),x) by A4, Th8;
thus ex_sup_of pi ((g .: A),x),(X --> T) . x by A9, A8, A7; :: thesis: verum

end;

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

A11: now :: thesis: for x being object st x in X holds
(sup (g .: A)) . x = (g . (sup A)) . x

let x be object ; :: 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 ;
commute g = f by A3, A2, FUNCT_6:57;
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;
then fx . (sup A) = (sup (g .: B)) . a by A5, A10, A12, YELLOW16:33;
hence (sup (g .: A)) . x = (g . (sup A)) . x by A3, A2, FUNCT_6:56; :: thesis: verum

end;

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

end;

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