consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A2: ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) ) by A1, Th14;
defpred S₁[ object ] means $1 in dom F;
deffunc H₁( object ) -> object = (a . $1) * ((M * F) . $1);
A3: for x being object st S₁[x] holds
H₁(x) in ExtREAL by XXREAL_0:def 1;
consider p being PartFunc of NAT,ExtREAL such that
A4: ( ( for x being object holds
( x in dom p iff ( x in NAT & S₁[x] ) ) ) & ( for x being object st x in dom p holds
p . x = H₁(x) ) ) from PARTFUN1:sch 3(A3);
for x being object st x in dom F holds
x in dom p by A4;
then A5: dom F c= dom p ;
for x being object st x in dom p holds
x in dom F by A4;
then dom p c= dom F ;
then A6: dom p = dom F by A5;
then dom p = Seg (len F) by FINSEQ_1:def 3;
then A7: p is FinSequence by FINSEQ_1:def 2;
rng p c= ExtREAL ;
then reconsider p = p as FinSequence of ExtREAL by A7, FINSEQ_1:def 4;
take Sum p ; :: thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x )
for n being Nat st n in dom p holds
p . n = (a . n) * ((M * F) . n) by A4;
hence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x ) by A2, A6; :: thesis: verum