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 u' = u as Element of A ;
thus (new_bi_fun d,q) . u,u = d . u',u' by Def11
.= Bottom L by A1, Def7 ; :: 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 Def11; :: thesis: verum

end;

end;

end;

hence new_bi_fun d,q is zeroed by Def7; :: thesis: verum