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 set st z in dom d holds
d . z = (new_bi_fun d,q) . z

proof

let z be set ; :: 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 set 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:106;
d . [x,y] = d . x9,y9
.= (new_bi_fun d,q) . x9,y9 by Def11
.= (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:119;
hence d c= new_bi_fun d,q by A2, GRFUNC_1:8; :: thesis: verum