let M be non empty set ; for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ M)
for i being Element of M holds (commute f) . i is directed-sups-preserving Function of S,T
let X, Y be non empty Poset; for f being directed-sups-preserving Function of X,(Y |^ M)
for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y
let f be directed-sups-preserving Function of X,(Y |^ M); for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y
let i be Element of M; (commute f) . i is directed-sups-preserving Function of X,Y
A1:
(M --> Y) . i = Y
;
dom (commute f) = M
by Lm1;
then A2:
(commute f) . i in rng (commute f)
by FUNCT_1:def 3;
A3:
f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y)))
by Lm1;
then
f is Function of the carrier of X,(Funcs (M, the carrier of Y))
by FUNCT_2:66;
then A4:
rng f c= Funcs (M, the carrier of Y)
by RELAT_1:def 19;
rng (commute f) c= Funcs ( the carrier of X, the carrier of Y)
by Lm1;
then consider g being Function such that
A5:
(commute f) . i = g
and
A6:
dom g = the carrier of X
and
A7:
rng g c= the carrier of Y
by A2, FUNCT_2:def 2;
reconsider g = g as Function of X,Y by A6, A7, FUNCT_2:2;
A8:
Y |^ M = product (M --> Y)
by YELLOW_1:def 5;
g is directed-sups-preserving
proof
let A be
Subset of
X;
WAYBEL_0:def 37 ( A is empty or not A is directed or g preserves_sup_of A )
assume
( not
A is
empty &
A is
directed )
;
g preserves_sup_of A
then reconsider B =
A as non
empty directed Subset of
X ;
assume A9:
ex_sup_of A,
X
;
WAYBEL_0:def 31 ( ex_sup_of g .: A,Y & "\/" ((g .: A),Y) = g . ("\/" (A,X)) )
A10:
f preserves_sup_of B
by WAYBEL_0:def 37;
then A11:
ex_sup_of f .: B,
Y |^ M
by A9;
then
ex_sup_of pi (
(f .: A),
i),
Y
by A8, A1, YELLOW16:31;
hence
ex_sup_of g .: A,
Y
by A4, A5, Th8;
"\/" ((g .: A),Y) = g . ("\/" (A,X))
A12:
pi (
(f .: A),
i)
= g .: A
by A4, A5, Th8;
sup (f .: B) = f . (sup B)
by A9, A10;
then
sup (pi ((f .: A),i)) = (f . (sup A)) . i
by A11, A8, A1, YELLOW16:33;
hence
"\/" (
(g .: A),
Y)
= g . ("\/" (A,X))
by A3, A5, A12, FUNCT_6:56;
verum
end;
hence
(commute f) . i is directed-sups-preserving Function of X,Y
by A5; verum