let S, T be lower-bounded complete LATTICE; for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
let f be monotone Function of S,T; for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
let x be Element of S; f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
deffunc H1( Element of S) -> Element of S = $1;
defpred S1[ Element of S] means $1 <= x;
defpred S2[ Element of S] means ex y1 being Element of S st
( $1 <= y1 & y1 in {x} );
A1:
the carrier of S c= dom f
by FUNCT_2:def 1;
A2:
f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] }
from WAYBEL24:sch 1(A1);
A3:
for x2 being Element of S holds
( S1[x2] iff S2[x2] )
proof
let x2 be
Element of
S;
( S1[x2] iff S2[x2] )
hereby ( S2[x2] implies S1[x2] )
end;
given y1 being
Element of
S such that A5:
(
x2 <= y1 &
y1 in {x} )
;
S1[x2]
thus
S1[
x2]
by A5, TARSKI:def 1;
verum
end;
{ H1(w) where w is Element of S : S1[w] } = { H1(x1) where x1 is Element of S : S2[x1] }
from WAYBEL24:sch 2(A3);
then A6:
downarrow x = { w where w is Element of S : w <= x }
by WAYBEL_0:14;
sup (f .: (downarrow x)) =
f . x
by Th4
.=
f . (sup (downarrow x))
by WAYBEL_0:34
;
hence
f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
by A2, A6, WAYBEL_0:34; verum