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

suppose S: S = {} ; :: thesis: ex b₁ being Function st
( dom b₁ = DOM S & ( for i being set st i in dom b₁ holds
b₁ . i = pi (S,i) ) )

take {} ; :: thesis: ( dom {} = DOM S & ( for i being set st i in dom {} holds
{} . i = pi (S,i) ) )
thus ( dom {} = DOM S & ( for i being set st i in dom {} holds
{} . i = pi (S,i) ) ) by S; :: thesis: verum

end;

suppose S <> {} ; :: thesis: ex b₁ being Function st
( dom b₁ = DOM S & ( for i being set st i in dom b₁ holds
b₁ . 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: ( dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) )
thus ( dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) ) by A2, A3; :: thesis: verum

end;

end;