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) holds commute f is Function of M,the carrier of (UPS S,T)
let X, Y be non empty Poset; :: thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds commute f is Function of M,the carrier of (UPS X,Y)
let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis: commute f is Function of M,the carrier of (UPS X,Y)
A1: ( rng (commute f) c= Funcs the carrier of X,the carrier of Y & dom (commute f) = M ) by Lm1;
rng (commute f) c= the carrier of (UPS X,Y)

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng (commute f) or g in the carrier of (UPS X,Y) )
assume g in rng (commute f) ; :: thesis: g in the carrier of (UPS X,Y)
then consider i being set such that
A2: ( i in dom (commute f) & g = (commute f) . i ) by FUNCT_1:def 5;
reconsider i = i as Element of M by A2, Lm1;
(commute f) . i is directed-sups-preserving Function of X,Y by Th38;
hence g in the carrier of (UPS X,Y) by A2, Def4; :: thesis: verum

end;

hence commute f is Function of M,the carrier of (UPS X,Y) by A1, FUNCT_2:4; :: thesis: verum