let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q)
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q)
let d be BiFunction of A,L; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q)
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: d c= new_bi_fun (d,q)
set g = new_bi_fun (d,q);
A1: A c= new_set A by XBOOLE_1:7;
A2: for z being object st z in dom d holds
d . z = (new_bi_fun (d,q)) . z

proof

let z be object ; :: thesis: ( z in dom d implies d . z = (new_bi_fun (d,q)) . z )
assume A3: z in dom d ; :: thesis: d . z = (new_bi_fun (d,q)) . z
then consider x, y being object such that
A4: [x,y] = z by RELAT_1:def 1;
reconsider x9 = x, y9 = y as Element of A by A3, A4, ZFMISC_1:87;
d . [x,y] = d . (x9,y9)
.= (new_bi_fun (d,q)) . (x9,y9) by Def10
.= (new_bi_fun (d,q)) . [x,y] ;
hence d . z = (new_bi_fun (d,q)) . z by A4; :: thesis: verum

end;

( dom d = [:A,A:] & dom (new_bi_fun (d,q)) = [:(new_set A),(new_set A):] ) by FUNCT_2:def 1;
then dom d c= dom (new_bi_fun (d,q)) by A1, ZFMISC_1:96;
hence d c= new_bi_fun (d,q) by A2, GRFUNC_1:2; :: thesis: verum