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

A3: 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;

now

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

suppose C1: 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 C1 ;
then f in { y where y is Function of B,A : y | Bo = yo } by C1;
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
D2: b0 in Bo by XBOOLE_0:def 1;
set f = (B --> (yo . b0)) +* yo;
C: rng ((B --> (yo . b0)) +* yo) c= (rng (B --> (yo . b0))) \/ (rng yo) by FUNCT_4:18;
E: rng (B --> (yo . b0)) c= {(yo . b0)} by FUNCOP_1:19;
B: dom yo = Bo by FUNCT_2:def 1;
yo . b0 in A by D2, FUNCT_2:7;
then {(yo . b0)} c= A by ZFMISC_1:37;
then D: rng (B --> (yo . b0)) c= A by E, XBOOLE_1:1;
rng yo c= A by RELSET_1:12;
then A: (rng (B --> (yo . b0))) \/ (rng yo) c= A by D, XBOOLE_1:8;
dom ((B --> (yo . b0)) +* yo) = (dom (B --> (yo . b0))) \/ Bo by B, FUNCT_4:def 1
.= B \/ Bo by FUNCOP_1:19
.= B by AS, XBOOLE_1:12 ;
then reconsider f = (B --> (yo . b0)) +* yo as Function of B,A by A, FUNCT_2:4, C, XBOOLE_1:1;
f | Bo = yo by B, 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;

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