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

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

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

( dom d = [:A,A:] & dom (new_bi_fun (d,q)) = [:(new_set A),(new_set A):] )
by FUNCT_2:def 1;
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;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

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