let A be non empty set ; 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_fun2 (d,q)
let L be 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_fun2 (d,q)
let d be BiFunction of A,L; for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun2 (d,q)
let q be Element of [:A,A, the carrier of L, the carrier of L:]; d c= new_bi_fun2 (d,q)
set g = new_bi_fun2 (d,q);
A1:
A c= new_set2 A
by XBOOLE_1:7;
A2:
for z being object st z in dom d holds
d . z = (new_bi_fun2 (d,q)) . z
proof
let z be
object ;
( z in dom d implies d . z = (new_bi_fun2 (d,q)) . z )
assume A3:
z in dom d
;
d . z = (new_bi_fun2 (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_fun2 (d,q)) . (
x9,
y9)
by Def4
.=
(new_bi_fun2 (d,q)) . [x,y]
;
hence
d . z = (new_bi_fun2 (d,q)) . z
by A4;
verum
end;
( dom d = [:A,A:] & dom (new_bi_fun2 (d,q)) = [:(new_set2 A),(new_set2 A):] )
by FUNCT_2:def 1;
then
dom d c= dom (new_bi_fun2 (d,q))
by A1, ZFMISC_1:96;
hence
d c= new_bi_fun2 (d,q)
by A2, GRFUNC_1:2; verum