per cases ( S = {} or S <> {} ) ;
suppose A1: S = {} ; :: thesis: ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . 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 A1; :: thesis: verum
end;
suppose S <> {} ; :: thesis: ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . 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 S2[ object , object ] means ex A being set st
( A = $1 & $2 = pi (S,A) );
A2: for e being object st e in meet { (dom f) where f is Element of S1 : verum } holds
ex u being object st S2[e,u]
proof
let e be object ; :: thesis: ( e in meet { (dom f) where f is Element of S1 : verum } implies ex u being object st S2[e,u] )
reconsider A = e as set by TARSKI:1;
assume e in meet { (dom f) where f is Element of S1 : verum } ; :: thesis: ex u being object st S2[e,u]
take u = pi (S,A); :: thesis: S2[e,u]
thus S2[e,u] ; :: thesis: verum
end;
consider g being Function such that
A3: dom g = meet { (dom f) where f is Element of S1 : verum } and
A4: for e being object st e in meet { (dom f) where f is Element of S1 : verum } holds
S2[e,g . e] from CLASSES1:sch 1(A2);
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 by A3; :: thesis: for i being set st i in dom g holds
g . i = pi (S,i)
let i be set ; :: thesis: ( i in dom g implies g . i = pi (S,i) )
assume i in dom g ; :: thesis: g . i = pi (S,i)
then S2[i,g . i] by A3, A4;
hence g . i = pi (S,i) ; :: thesis: verum
end;
end;