let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is zeroed
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is zeroed
let d be BiFunction of A,L; :: thesis: ( d is zeroed implies for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is zeroed )
assume A1: d is zeroed ; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is zeroed
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: new_bi_fun (d,q) is zeroed
set f = new_bi_fun (d,q);
for u being Element of new_set A holds (new_bi_fun (d,q)) . (u,u) = Bottom L

proof

let u be Element of new_set A; :: thesis: (new_bi_fun (d,q)) . (u,u) = Bottom L
A2: ( u in A or u in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;

per cases ( u in A or u = {A} or u = {{A}} or u = {{{A}}} ) by A2, ENUMSET1:def 1;

suppose u in A ; :: thesis: (new_bi_fun (d,q)) . (u,u) = Bottom L

then reconsider u9 = u as Element of A ;
thus (new_bi_fun (d,q)) . (u,u) = d . (u9,u9) by Def10
.= Bottom L by A1 ; :: thesis: verum

end;

suppose ( u = {A} or u = {{A}} or u = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (u,u) = Bottom L

hence (new_bi_fun (d,q)) . (u,u) = Bottom L by Def10; :: thesis: verum

end;

end;

end;

hence new_bi_fun (d,q) is zeroed ; :: thesis: verum