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

proof

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

proof

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

end;

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

end;

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