defpred S₁[ object , object ] means for x being set st x = $1 holds
$2 = Sum (f . x);
A1: for e being object st e in dom f holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in dom f implies ex u being object st S₁[e,u] )
assume e in dom f ; :: thesis: ex u being object st S₁[e,u]
then reconsider E = e as set ;
take s = Sum (f . E); :: thesis: S₁[e,s]
thus S₁[e,s] ; :: thesis: verum

end;

consider s being Function such that
A2: ( dom s = dom f & ( for e being object st e in dom f holds
S₁[e,s . e] ) ) from CLASSES1:sch 1(A1);
rng s c= COMPLEX

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in COMPLEX )
assume y in rng s ; :: thesis: y in COMPLEX
then consider x being object such that
A3: ( x in dom s & s . x = y ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
s . x = Sum (f . x) by A3, A2;
hence y in COMPLEX by A3, XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider s = s as complex-valued Function by VALUED_0:def 1;
take s ; :: thesis: ( dom s = dom f & ( for x being set holds s . x = Sum (f . x) ) )
thus dom s = dom f by A2; :: thesis: for x being set holds s . x = Sum (f . x)
let x be set ; :: thesis: s . x = Sum (f . x)

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: s . x = Sum (f . x)

hence s . x = Sum (f . x) by A2; :: thesis: verum

end;

suppose A4: not x in dom f ; :: thesis: s . x = Sum (f . x)

then Sum (f . x) = 0 by RVSUM_2:29, FUNCT_1:def 2;
hence s . x = Sum (f . x) by A4, A2, FUNCT_1:def 2; :: thesis: verum

end;

end;