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}},} ) by XBOOLE_0:def 3;
per cases ( u in A or u = {A} or u = {{A}} or u = ) by ;
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 = ) ; :: 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