A1: the carrier of (L |^ X) = Funcs X,the carrier of L by YELLOW_1:28;
( dom (X --> (Bottom L)) = X & rng (X --> (Bottom L)) c= the carrier of L ) by FUNCT_2:def 1;
then reconsider f = X --> (Bottom L) as Element of (L |^ X) by A1, FUNCT_2:def 2;
take f ; :: according to YELLOW_0:def 4 :: thesis: f is_<=_than the carrier of (L |^ X)
let g be Element of (L |^ X); :: according to LATTICE3:def 8 :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

then L |^ X = RelStr(# {{} },(id {{} }) #) by YELLOW_1:27;
then ( f <= f & f = {} & g = {} ) by TARSKI:def 1;
hence ( not g in the carrier of (L |^ X) or f <= g ) ; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ( not g in the carrier of (L |^ X) or f <= g )

then reconsider X = X as non empty set ;
reconsider f = f, g = g as Element of (L |^ X) ;

now

let x be Element of X; :: thesis: f . x <= g . x
( f . x = Bottom L & L is lower-bounded ) by FUNCOP_1:13;
hence f . x <= g . x by YELLOW_0:44; :: thesis: verum

end;

hence ( not g in the carrier of (L |^ X) or f <= g ) by WAYBEL27:14; :: thesis: verum

end;

end;