let Q, P be non empty strict chain-complete Poset; :: thesis: for z being Element of Q holds P --> z is continuous
let z be Element of Q; :: thesis: P --> z is continuous
set IT = P --> z;
for L being non empty Chain of P holds (P --> z) . (sup L) = sup ((P --> z) .: L)

proof

let L be non empty Chain of P; :: thesis: (P --> z) . (sup L) = sup ((P --> z) .: L)
set M = (P --> z) .: L;
for x being Element of Q st x in (P --> z) .: L holds
x <= z

proof

let x be Element of Q; :: thesis: ( x in (P --> z) .: L implies x <= z )
assume x in (P --> z) .: L ; :: thesis: x <= z
then consider a being set such that
D1: ( a in dom (P --> z) & a in L & x = (P --> z) . a ) by FUNCT_1:def 12;
thus x <= z by D1, FUNCOP_1:13; :: thesis: verum

end;

then B3: (P --> z) .: L is_<=_than z by LATTICE3:def 9;
for y being Element of Q st (P --> z) .: L is_<=_than y holds
z <= y

proof

let y be Element of Q; :: thesis: ( (P --> z) .: L is_<=_than y implies z <= y )
assume D1: (P --> z) .: L is_<=_than y ; :: thesis: z <= y
consider a being set such that
D2: a in L by XBOOLE_0:def 1;
a in the carrier of P by D2;
then D3: a in dom (P --> z) by FUNCOP_1:19;
(P --> z) . a = z by D2, FUNCOP_1:13;
then z in (P --> z) .: L by D2, D3, FUNCT_1:def 12;
hence z <= y by D1, LATTICE3:def 9; :: thesis: verum

end;

then z = "\/" (((P --> z) .: L),Q) by B3, YELLOW_0:30;
hence (P --> z) . (sup L) = sup ((P --> z) .: L) by FUNCOP_1:13; :: thesis: verum

end;

hence P --> z is continuous by Thcontinuous01; :: thesis: verum