let K be Field; for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
let V1 be finite-dimensional VectSp of K; for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
let B1 be FinSequence of V1; for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
let W1 be Subspace of V1; for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
let B2 be FinSequence of W1; ( B1 = B2 implies Sum B1 = Sum B2 )
assume A1:
B1 = B2
; Sum B1 = Sum B2
defpred S1[ Nat] means for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 & len B1 = $1 holds
Sum B1 = Sum B2;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let B1 be
FinSequence of
V1;
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 & len B1 = n + 1 holds
Sum B1 = Sum B2let W1 be
Subspace of
V1;
for B2 being FinSequence of W1 st B1 = B2 & len B1 = n + 1 holds
Sum B1 = Sum B2let B2 be
FinSequence of
W1;
( B1 = B2 & len B1 = n + 1 implies Sum B1 = Sum B2 )
assume that A4:
B1 = B2
and A5:
len B1 = n + 1
;
Sum B1 = Sum B2
A6:
len (B1 | n) = n
by A5, FINSEQ_1:59, NAT_1:11;
then A7:
Sum (B1 | n) = Sum (B2 | n)
by A3, A4;
1
<= n + 1
by NAT_1:11;
then A8:
n + 1
in dom B1
by A5, FINSEQ_3:25;
then A9:
B2 . (n + 1) = B2 /. (n + 1)
by A4, PARTFUN1:def 6;
A10:
B1 . (n + 1) = B1 /. (n + 1)
by A8, PARTFUN1:def 6;
A11:
dom (B1 | n) = Seg n
by A6, FINSEQ_1:def 3;
hence Sum B1 =
(Sum (B1 | n)) + (B1 /. (n + 1))
by A5, A10, A6, RLVECT_1:38
.=
(Sum (B2 | n)) + (B2 /. (n + 1))
by A4, A10, A9, A7, VECTSP_4:13
.=
Sum B2
by A4, A5, A9, A6, A11, RLVECT_1:38
;
verum
end;
A12:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A2);
then
S1[ len B1]
;
hence
Sum B1 = Sum B2
by A1; verum