let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps S,T) = S --> (Bottom T)
let T be non empty reflexive antisymmetric lower-bounded RelStr ; :: thesis: Bottom (MonMaps S,T) = S --> (Bottom T)
set L = MonMaps S,T;
reconsider f = S --> (Bottom T) as Element of (MonMaps S,T) by WAYBEL10:10;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps S,T) st b is_>=_than {} holds
f <= b

proof

let b be Element of (MonMaps S,T); :: thesis: ( b is_>=_than {} implies f <= b )
assume b is_>=_than {} ; :: thesis: f <= b
reconsider b9 = b as Function of S,T by WAYBEL10:10;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:59;
for x being Element of S holds f9 . x <= b9 . x

proof

let x be Element of S; :: thesis: f9 . x <= b9 . x
f9 . x = (the carrier of S --> (Bottom T)) . x
.= Bottom T by FUNCOP_1:13 ;
hence f9 . x <= b9 . x by YELLOW_0:44; :: thesis: verum

end;

then f9 <= b9 by YELLOW_2:10;
then f99 <= b99 by WAYBEL10:12;
hence f <= b by YELLOW_0:61; :: thesis: verum

end;

f is_>=_than {} by YELLOW_0:6;
then f = "\/" {} ,(MonMaps S,T) by A1, YELLOW_0:30;
hence Bottom (MonMaps S,T) = S --> (Bottom T) by YELLOW_0:def 11; :: thesis: verum