let n be Nat; for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
set T = TOP-REAL n;
set V = n -VectSp_over F_Real;
let F be FinSequence of (TOP-REAL n); for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
let Fv be FinSequence of (n -VectSp_over F_Real); ( 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 (n -VectSp_over F_Real) such that
A5:
Sum Fv = fv . (len Fv)
and
A6:
fv . 0 = 0. (n -VectSp_over F_Real)
and
A7:
for j being Nat
for v being Element of (n -VectSp_over F_Real) 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;
reconsider Fvi1 =
Fv /. (i + 1),
fvi =
fv . i as
Element of
n -tuples_on the
carrier of
F_Real by MATRIX13:102;
A10:
(
@ (@ Fvi1) = Fvi1 &
@ (@ fvi) = fvi )
;
reconsider Fi1 =
F /. (i + 1) as
Element of
T ;
assume A11:
i + 1
<= len F
;
f . (i + 1) = fv . (i + 1)
then A12:
i < len F
by NAT_1:13;
1
<= i + 1
by NAT_1:11;
then A13:
i + 1
in dom F
by A11, FINSEQ_3:25;
then
F . (i + 1) = F /. (i + 1)
by PARTFUN1:def 6;
then A14:
f . (i + 1) = (f . i) + Fi1
by A4, A12;
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) =
(@ fvi) + (@ Fvi1)
by A9, A11, A14, EUCLID:64, NAT_1:13
.=
fvi + Fvi1
by A10, MATRTOP1:1
.=
(fv . i) + (Fv /. (i + 1))
by MATRIX13:102
.=
fv . (i + 1)
by A1, A7, A12, 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