let D be non empty set ; :: thesis: for T being FinSequence of D
for f being Function of D,NAT holds Sum (f * T) is Nat
let T be FinSequence of D; :: thesis: for f being Function of D,NAT holds Sum (f * T) is Nat
let f be Function of D,NAT; :: thesis: Sum (f * T) is Nat
defpred S₁[ FinSequence of REAL ] means ( $1 is FinSequence of NAT implies Sum $1 is Nat );
A1: S₁[ <*> REAL] by RVSUM_1:72;
A2: for p being FinSequence of REAL
for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
assume p ^ <*x*> is FinSequence of NAT ; :: thesis: Sum (p ^ <*x*>) is Nat
then A4: rng (p ^ <*x*>) c= NAT by FINSEQ_1:def 4;
rng p c= rng (p ^ <*x*>) by FINSEQ_1:29;
then A5: rng p c= NAT by A4;
rng <*x*> c= rng (p ^ <*x*>) by FINSEQ_1:30;
then A6: rng <*x*> c= NAT by A4;
rng <*x*> = {x} by FINSEQ_1:38;
then reconsider n = x as Element of NAT by A6, ZFMISC_1:31;
reconsider s = Sum p as Nat by A3, A5, FINSEQ_1:def 4;
Sum (p ^ <*x*>) = s + n by RVSUM_1:74;
hence Sum (p ^ <*x*>) is Nat ; :: thesis: verum

end;

A7: for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A1, A2);
f * T is FinSequence of NAT by FINSEQ_2:32;
hence Sum (f * T) is Nat by A7; :: thesis: verum