set D = { y where y is Function of B,A : y | Bo = yo } ;
A2:
now not { y where y is Function of B,A : y | Bo = yo } is empty per cases
( Bo = {} or Bo <> {} )
;
suppose
Bo <> {}
;
not { y where y is Function of B,A : y | Bo = yo } is empty then consider b0 being
object such that A4:
b0 in Bo
by XBOOLE_0:def 1;
yo . b0 in A
by A4, FUNCT_2:5;
then A5:
{(yo . b0)} c= A
by ZFMISC_1:31;
set f =
(B --> (yo . b0)) +* yo;
A6:
rng ((B --> (yo . b0)) +* yo) c= (rng (B --> (yo . b0))) \/ (rng yo)
by FUNCT_4:17;
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:13
.=
B
by A1, XBOOLE_1:12
;
rng (B --> (yo . b0)) c= {(yo . b0)}
by FUNCOP_1:13;
then
rng (B --> (yo . b0)) c= A
by A5;
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:2, XBOOLE_1:1;
f | Bo = yo
by A8, FUNCT_4:23;
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
;
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; verum