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= 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) and
A3: 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 A3, Def4; :: thesis: verum

end;

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