thus ( not S is empty implies ex g being Function st
( ( for x being set holds
( x in dom g iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom g holds
g . i = pi S,i ) ) ) :: thesis: ( S is empty implies ex b₁ being Function st b₁ = {} )

proof

assume not S is empty ; :: thesis: ex g being Function st
( ( for x being set holds
( x in dom g iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom g holds
g . i = pi S,i ) )
then reconsider S1 = S as non empty functional set ;
set D = { (dom f) where f is Element of S1 : verum } ;
defpred S₂[ set , set ] means $2 = pi S,$1;
A1: for e being set st e in meet { (dom f) where f is Element of S1 : verum } holds
ex u being set st S₂[e,u] ;
consider g being Function such that
A2: dom g = meet { (dom f) where f is Element of S1 : verum } and
A3: for e being set st e in meet { (dom f) where f is Element of S1 : verum } holds
S₂[e,g . e] from CLASSES1:sch 1(A1);
take g ; :: thesis: ( ( for x being set holds
( x in dom g iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom g holds
g . i = pi S,i ) )

hereby :: thesis: for i being set st i in dom g holds
g . i = pi S,i

let x be set ; :: thesis: ( ( x in dom g implies for f being Function st f in S holds
x in dom f ) & ( ( for f being Function st f in S holds
x in dom f ) implies x in dom g ) )

hereby :: thesis: ( ( for f being Function st f in S holds
x in dom f ) implies x in dom g )

assume A4: x in dom g ; :: thesis: for f being Function st f in S holds
x in dom f
let f be Function; :: thesis: ( f in S implies x in dom f )
assume f in S ; :: thesis: x in dom f
then dom f in { (dom f) where f is Element of S1 : verum } ;
hence x in dom f by A2, A4, SETFAM_1:def 1; :: thesis: verum

end;

assume A5: for f being Function st f in S holds
x in dom f ; :: thesis: x in dom g
consider f being Element of S1;
A6: dom f in { (dom f) where f is Element of S1 : verum } ;
for Y being set st Y in { (dom f) where f is Element of S1 : verum } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { (dom f) where f is Element of S1 : verum } implies x in Y )
assume Y in { (dom f) where f is Element of S1 : verum } ; :: thesis: x in Y
then ex f being Element of S1 st Y = dom f ;
hence x in Y by A5; :: thesis: verum

end;

hence x in dom g by A2, A6, SETFAM_1:def 1; :: thesis: verum

end;

thus for i being set st i in dom g holds
g . i = pi S,i by A2, A3; :: thesis: verum

end;

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