let n be Nat; for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv
set T = TOP-REAL n;
set V = RealVectSpace (Seg n);
let F be FinSequence of (TOP-REAL n); for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv
let Fv be FinSequence of (RealVectSpace (Seg n)); ( Fv = F implies Sum F = Sum Fv )
assume A1:
Fv = F
; Sum F = Sum Fv
reconsider T = TOP-REAL n as RealLinearSpace ;
consider f being sequence of the carrier of T such that
A2:
Sum F = f . (len F)
and
A3:
f . 0 = 0. T
and
A4:
for j being Nat
for v being Element of T st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
consider fv being sequence of the carrier of (RealVectSpace (Seg n)) such that
A5:
Sum Fv = fv . (len Fv)
and
A6:
fv . 0 = 0. (RealVectSpace (Seg n))
and
A7:
for j being Nat
for v being Element of (RealVectSpace (Seg n)) st j < len Fv & v = Fv . (j + 1) holds
fv . (j + 1) = (fv . j) + v
by RLVECT_1:def 12;
defpred S1[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A9:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
A10:
the
carrier of
(n -VectSp_over F_Real) = the
carrier of
(TOP-REAL n)
the
carrier of
(n -VectSp_over F_Real) = n -tuples_on the
carrier of
F_Real
by MATRIX13:102;
then reconsider Fvi1 =
Fv /. (i + 1),
fvi =
fv . i as
Element of
n -tuples_on the
carrier of
F_Real by A10, Lm1;
reconsider Fi1 =
F /. (i + 1) as
Element of
T ;
assume A11:
i + 1
<= len F
;
f . (i + 1) = fv . (i + 1)
A13:
i + 1
in dom F
by A11, NAT_1:11, FINSEQ_3:25;
then
F . (i + 1) = F /. (i + 1)
by PARTFUN1:def 6;
then A14:
f . (i + 1) = (f . i) + Fi1
by A4, A11, NAT_1:13;
A15:
Fv /. (i + 1) = Fv . (i + 1)
by A1, A13, PARTFUN1:def 6;
then
Fvi1 = F /. (i + 1)
by A1, A13, PARTFUN1:def 6;
hence f . (i + 1) =
(fv . i) + (Fv /. (i + 1))
by A9, A11, A14, EUCLID:64, NAT_1:13
.=
fv . (i + 1)
by A1, A7, A11, NAT_1:13, A15
;
verum
end;
A16:
S1[ 0 ]
by A3, A6, Lm2;
for n being Nat holds S1[n]
from NAT_1:sch 2(A16, A8);
hence
Sum F = Sum Fv
by A1, A2, A5; verum