A1:
rng (X --> (Bottom L)) c= the carrier of L
;

( the carrier of (L |^ X) = Funcs (X, the carrier of L) & dom (X --> (Bottom L)) = X ) by YELLOW_1:28;

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 )

( the carrier of (L |^ X) = Funcs (X, the carrier of L) & dom (X --> (Bottom L)) = X ) by YELLOW_1:28;

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 )
;

end;

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

A3:
f <= f
;

( L |^ X = RelStr(# {{}},(id {{}}) #) & f = {} ) by A2, YELLOW_1:27;

hence ( not g in the carrier of (L |^ X) or f <= g ) by A3, TARSKI:def 1; :: thesis: verum

end;( L |^ X = RelStr(# {{}},(id {{}}) #) & f = {} ) by A2, YELLOW_1:27;

hence ( not g in the carrier of (L |^ X) or f <= g ) by A3, TARSKI:def 1; :: thesis: verum

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) ;

end;reconsider f = f, g = g as Element of (L |^ X) ;

now :: thesis: for x being Element of X holds f . x <= g . x

hence
( not g in the carrier of (L |^ X) or f <= g )
by WAYBEL27:14; :: thesis: verumlet x be Element of X; :: thesis: f . x <= g . x

thus f . x <= g . x by YELLOW_0:44; :: thesis: verum

end;thus f . x <= g . x by YELLOW_0:44; :: thesis: verum