let V be RealLinearSpace; :: thesis: for f being Functional of V
for s being FinSequence of V st f is additive holds
f . (Sum s) = Sum (f * s)
let f be Functional of V; :: thesis: for s being FinSequence of V st f is additive holds
f . (Sum s) = Sum (f * s)
let s be FinSequence of V; :: thesis: ( f is additive implies f . (Sum s) = Sum (f * s) )
assume A1: f is additive ; :: thesis: f . (Sum s) = Sum (f * s)
defpred S₁[ Nat] means for V being RealLinearSpace
for f being Functional of V
for s being FinSequence of V st len s = $1 & f is additive holds
f . (Sum s) = Sum (f * s);
A2: S₁[ 0 ]

proof

let V be RealLinearSpace; :: thesis: for f being Functional of V
for s being FinSequence of V st len s = 0 & f is additive holds
f . (Sum s) = Sum (f * s)
let f be Functional of V; :: thesis: for s being FinSequence of V st len s = 0 & f is additive holds
f . (Sum s) = Sum (f * s)
let s be FinSequence of V; :: thesis: ( len s = 0 & f is additive implies f . (Sum s) = Sum (f * s) )
assume that
A3: len s = 0 and
A4: f is additive ; :: thesis: f . (Sum s) = Sum (f * s)
B5: Sum s = 0. V by A3, RLVECT_1:75;
dom f = the carrier of V by FUNCT_2:def 1;
then rng s c= dom f ;
then dom (f * s) = dom s by RELAT_1:27
.= Seg (len s) by FINSEQ_1:def 3 ;
then len (f * s) = 0 by A3, FINSEQ_1:def 3;
then f * s = <*> REAL ;
hence f . (Sum s) = Sum (f * s) by B5, A4, HAHNBAN:20, RVSUM_1:72; :: thesis: verum

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
let V be RealLinearSpace; :: thesis: for f being Functional of V
for s being FinSequence of V st len s = n + 1 & f is additive holds
f . (Sum s) = Sum (f * s)
let f be Functional of V; :: thesis: for s being FinSequence of V st len s = n + 1 & f is additive holds
f . (Sum s) = Sum (f * s)
let s be FinSequence of V; :: thesis: ( len s = n + 1 & f is additive implies f . (Sum s) = Sum (f * s) )
assume that
A8: len s = n + 1 and
A9: f is additive ; :: thesis: f . (Sum s) = Sum (f * s)
set s0 = s | n;
set p = f * s;
B10: dom s = Seg (n + 1) by A8, FINSEQ_1:def 3;
then s . (n + 1) in rng s by FUNCT_1:3, FINSEQ_1:4;
then reconsider v = s . (n + 1) as Point of V ;
A11: n = len (s | n) by A8, FINSEQ_1:59, NAT_1:11;
then B12: s | n = s | (dom (s | n)) by FINSEQ_1:def 3;
A13: f . (s . (n + 1)) = (f * s) . (n + 1) by B10, FINSEQ_1:4, FUNCT_1:13;
A15: f . (Sum s) = f . ((Sum (s | n)) + v) by B12, A8, A11, RLVECT_1:38
.= (f . (Sum (s | n))) + (f . (s . (n + 1))) by A9, HAHNBAN:def 2
.= (Sum (f * (s | n))) + ((f * s) . (n + 1)) by A13, A7, A9, A11 ;
dom f = the carrier of V by FUNCT_2:def 1;
then rng s c= dom f ;
then B18: dom (f * s) = dom s by RELAT_1:27
.= Seg (len s) by FINSEQ_1:def 3 ;
then A17: len (f * s) = n + 1 by A8, FINSEQ_1:def 3;
A18: ( 1 <= n + 1 & n + 1 <= len (f * s) ) by NAT_1:11, B18, A8, FINSEQ_1:def 3;
f * s = ((f * s) | n) ^ <*((f * s) /. (n + 1))*> by A17, FINSEQ_5:21;
then f * s = ((f * s) | n) ^ <*((f * s) . (n + 1))*> by A18, FINSEQ_4:15;
then Sum (f * s) = (Sum ((f * s) | n)) + ((f * s) . (n + 1)) by RVSUM_1:74;
hence f . (Sum s) = Sum (f * s) by A15, RELAT_1:83; :: thesis: verum

end;

A19: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
len s is Nat ;
hence f . (Sum s) = Sum (f * s) by A1, A19; :: thesis: verum