thus ( not D is empty implies ex F being Function st
( dom F = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
F . <*x,y*> = f . (x,y) ) ) ) :: thesis: ( D is empty implies ex b₁ being Function st b₁ = {} )

proof

assume not D is empty ; :: thesis: ex F being Function st
( dom F = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
F . <*x,y*> = f . (x,y) ) )
defpred S₁[ object , object ] means ex x, y being object st
( $1 = <*x,y*> & $2 = f . (x,y) );
set X = 2 -tuples_on D;
A1: for e being object st e in 2 -tuples_on D holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in 2 -tuples_on D implies ex u being object st S₁[e,u] )
assume e in 2 -tuples_on D ; :: thesis: ex u being object st S₁[e,u]
then consider x, y being object such that
( x in D & y in D ) and
A2: e = <*x,y*> by FINSEQ_2:137;
take f . (x,y) ; :: thesis: S₁[e,f . (x,y)]
thus S₁[e,f . (x,y)] by A2; :: thesis: verum

end;

consider F being Function such that
A3: dom F = 2 -tuples_on D and
A4: for e being object st e in 2 -tuples_on D holds
S₁[e,F . e] from CLASSES1:sch 1(A1);
take F ; :: thesis: ( dom F = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
F . <*x,y*> = f . (x,y) ) )
thus dom F = 2 -tuples_on D by A3; :: thesis: for x, y being object st [x,y] in dom f holds
F . <*x,y*> = f . (x,y)
let e1, e2 be object ; :: thesis: ( [e1,e2] in dom f implies F . <*e1,e2*> = f . (e1,e2) )
assume [e1,e2] in dom f ; :: thesis: F . <*e1,e2*> = f . (e1,e2)
then ( e1 in D & e2 in D ) by ZFMISC_1:87;
then consider x, y being object such that
A5: <*e1,e2*> = <*x,y*> and
A6: F . <*e1,e2*> = f . (x,y) by A4, FINSEQ_2:101;
( e1 = x & e2 = y ) by A5, FINSEQ_1:77;
hence F . <*e1,e2*> = f . (e1,e2) by A6; :: thesis: verum

end;

thus ( D is empty implies ex b₁ being Function st b₁ = {} ) ; :: thesis: verum