let P, Q be non empty strict chain-complete Poset; :: thesis: for L being non empty Chain of P
for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)
let L be non empty Chain of P; :: thesis: for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)
let f be monotone Function of P,Q; :: thesis: sup (f .: L) <= f . (sup L)
reconsider M = f .: L as non empty Chain of Q by Th1;
set r = sup L;
set u = f . (sup L);
A1: ( ex_sup_of L,P & ex_sup_of M,Q ) by Def1;
for q being Element of Q st q in M holds
q <= f . (sup L)

proof

let q be Element of Q; :: thesis: ( q in M implies q <= f . (sup L) )
assume q in M ; :: thesis: q <= f . (sup L)
then consider x being object such that
A2: ( x in dom f & x in L & q = f . x ) by FUNCT_1:def 6;
reconsider x = x as Element of P by A2;
L is_<=_than sup L by A1, YELLOW_0:def 9;
then x <= sup L by A2;
hence q <= f . (sup L) by A2, ORDERS_3:def 5; :: thesis: verum

end;

then M is_<=_than f . (sup L) ;
hence sup (f .: L) <= f . (sup L) by A1, YELLOW_0:def 9; :: thesis: verum