set D = { y where y is Function of B,A : y | Bo = yo } ;

A2: now

per cases ( Bo = {} or Bo <> {} ) ;

suppose A3: Bo = {} ; :: thesis: not { y where y is Function of B,A : y | Bo = yo } is empty

consider f being Function of B,A;
f | {} = {}
.= yo by A3 ;
then f in { y where y is Function of B,A : y | Bo = yo } by A3;
hence not { y where y is Function of B,A : y | Bo = yo } is empty ; :: thesis: verum

end;

suppose Bo <> {} ; :: thesis: not { y where y is Function of B,A : y | Bo = yo } is empty

then consider b0 being set such that
A4: b0 in Bo by XBOOLE_0:def 1;
yo . b0 in A by A4, FUNCT_2:7;
then A5: {(yo . b0)} c= A by ZFMISC_1:37;
set f = (B --> (yo . b0)) +* yo;
A6: rng ((B --> (yo . b0)) +* yo) c= (rng (B --> (yo . b0))) \/ (rng yo) by FUNCT_4:18;
A7: rng yo c= A by RELAT_1:def 19;
A8: dom yo = Bo by FUNCT_2:def 1;
then A9: dom ((B --> (yo . b0)) +* yo) = (dom (B --> (yo . b0))) \/ Bo by FUNCT_4:def 1
.= B \/ Bo by FUNCOP_1:19
.= B by A1, XBOOLE_1:12 ;
rng (B --> (yo . b0)) c= {(yo . b0)} by FUNCOP_1:19;
then rng (B --> (yo . b0)) c= A by A5, XBOOLE_1:1;
then (rng (B --> (yo . b0))) \/ (rng yo) c= A by A7, XBOOLE_1:8;
then reconsider f = (B --> (yo . b0)) +* yo as Function of B,A by A6, A9, FUNCT_2:4, XBOOLE_1:1;
f | Bo = yo by A8, FUNCT_4:24;
then f in { y where y is Function of B,A : y | Bo = yo } ;
hence not { y where y is Function of B,A : y | Bo = yo } is empty ; :: thesis: verum

end;

end;

end;

now

let z be set ; :: thesis: ( z in { y where y is Function of B,A : y | Bo = yo } implies z in Funcs B,A )
assume z in { y where y is Function of B,A : y | Bo = yo } ; :: thesis: z in Funcs B,A
then ex y being Function of B,A st
( z = y & y | Bo = yo ) ;
hence z in Funcs B,A by FUNCT_2:11; :: thesis: verum

end;

hence { y where y is Function of B,A : y | Bo = yo } is non empty Subset of (Funcs B,A) by A2, TARSKI:def 3; :: thesis: verum