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

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

hence
new_bi_fun (d,q) is zeroed
; :: thesis: verum
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;

end;A2: ( u in A or u in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;