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 object ; :: 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 object such that
A2: i in dom (commute f) and
A3: g = (commute f) . i by FUNCT_1:def 3;
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:2; :: thesis: verum