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_fun2 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_fun2 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_fun2 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_fun2 d,q is zeroed
let q be Element of [:A,A,the carrier of L,the carrier of L:]; :: thesis: new_bi_fun2 d,q is zeroed
set f = new_bi_fun2 d,q;
for u being Element of new_set2 A holds (new_bi_fun2 d,q) . u,u = Bottom L

proof

let u be Element of new_set2 A; :: thesis: (new_bi_fun2 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}} ) by A2, TARSKI:def 2;

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

then reconsider u' = u as Element of A ;
thus (new_bi_fun2 d,q) . u,u = d . u',u' by Def5
.= Bottom L by A1, LATTICE5:def 7 ; :: thesis: verum

end;

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

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

end;

end;

end;

hence new_bi_fun2 d,q is zeroed by LATTICE5:def 7; :: thesis: verum