defpred S₁[ Element of divs A, set ] means ex D being Division of A st
( D = $1 & $2 = upper_sum f,D );
consider g being PartFunc of (divs A),REAL such that
A1: for d being Element of divs A holds
( d in dom g iff ex c being Element of REAL st S₁[d,c] ) and
A2: for d being Element of divs A st d in dom g holds
S₁[d,g . d] from SEQ_1:sch 2();
take g ; :: thesis: ( dom g = divs A & ( for D being Division of A st D in dom g holds
g . D = upper_sum f,D ) )
thus dom g c= divs A ; :: according to XBOOLE_0:def 10 :: thesis: ( divs A c= dom g & ( for D being Division of A st D in dom g holds
g . D = upper_sum f,D ) )
thus divs A c= dom g :: thesis: for D being Division of A st D in dom g holds
g . D = upper_sum f,D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in divs A or x in dom g )
assume x in divs A ; :: thesis: x in dom g
then reconsider x = x as Element of divs A ;
reconsider D = x as Division of A by Def3;
S₁[x, upper_sum f,D] ;
hence x in dom g by A1; :: thesis: verum

end;

let D be Division of A; :: thesis: ( D in dom g implies g . D = upper_sum f,D )
reconsider D1 = D as Element of divs A by Def3;
assume D in dom g ; :: thesis: g . D = upper_sum f,D
then S₁[D1,g . D1] by A2;
hence g . D = upper_sum f,D ; :: thesis: verum