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: 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;
A2: the carrier of (T |^ X) = Funcs X,the carrier of T by YELLOW_1:28;
A3: f in Funcs X,the carrier of (UPS S,T) by FUNCT_2:11;
then commute f in Funcs the carrier of S,(Funcs X,the carrier of T) by A1, FUNCT_6:85;
then reconsider g = commute f as Function of S,(T |^ X) by A2, FUNCT_2:121;
A4: rng g c= Funcs X,the carrier of T by A2;
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 ;
assume A5: 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) )
A6: T |^ X = product (X --> T) by YELLOW_1:def 5;

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;
A7: (X --> T) . x = T by FUNCOP_1:13;
( commute g = f & dom f = X ) by A1, A3, FUNCT_2:def 1, FUNCT_6:87;
then ( fx .: A = pi (g .: A),x & fx preserves_sup_of B ) by A4, Th8, WAYBEL_0:def 37;
hence ex_sup_of pi (g .: A),x,(X --> T) . x by A5, A7, WAYBEL_0:def 31; :: thesis: verum

end;

hence A8: ex_sup_of g .: A,T |^ X by A6, YELLOW16:33; :: thesis: "\/" (g .: A),(T |^ X) = g . ("\/" A,S)
A9: ( dom (sup (g .: A)) = X & dom (g . (sup A)) = X ) by A6, WAYBEL_3:27;

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;
A10: (X --> T) . a = T by FUNCOP_1:13;
( commute g = f & dom f = X ) by A1, A3, FUNCT_2:def 1, FUNCT_6:87;
then ( fx .: A = pi (g .: A),a & fx preserves_sup_of B ) by A4, Th8, WAYBEL_0:def 37;
then sup (pi (g .: B),a) = fx . (sup A) by A5, WAYBEL_0:def 31;
then fx . (sup A) = (sup (g .: B)) . a by A6, A8, A10, YELLOW16:35;
hence (sup (g .: A)) . x = (g . (sup A)) . x by A1, A3, FUNCT_6:86; :: thesis: verum

end;

hence "\/" (g .: A),(T |^ X) = g . ("\/" A,S) by A9, FUNCT_1:9; :: thesis: verum

end;

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