let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
let B2 be FinSequence of W1; :: thesis: ( B1 = B2 implies Sum B1 = Sum B2 )
assume A1: B1 = B2 ; :: thesis: Sum B1 = Sum B2
defpred S₁[ 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: S₁[ 0 ]

proof

let B1 be FinSequence of V1; :: thesis: for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 & len B1 = 0 holds
Sum B1 = Sum B2
let W1 be Subspace of V1; :: thesis: for B2 being FinSequence of W1 st B1 = B2 & len B1 = 0 holds
Sum B1 = Sum B2
let B2 be FinSequence of W1; :: thesis: ( B1 = B2 & len B1 = 0 implies Sum B1 = Sum B2 )
assume A3: ( B1 = B2 & len B1 = 0 ) ; :: thesis: Sum B1 = Sum B2
( Sum B1 = 0. V1 & Sum B2 = 0. W1 ) by A3, RLVECT_1:94;
hence Sum B1 = Sum B2 by VECTSP_4:19; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let B1 be FinSequence of V1; :: thesis: for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 & len B1 = n + 1 holds
Sum B1 = Sum B2
let W1 be Subspace of V1; :: thesis: for B2 being FinSequence of W1 st B1 = B2 & len B1 = n + 1 holds
Sum B1 = Sum B2
let B2 be FinSequence of W1; :: thesis: ( B1 = B2 & len B1 = n + 1 implies Sum B1 = Sum B2 )
assume A6: ( B1 = B2 & len B1 = n + 1 ) ; :: thesis: Sum B1 = Sum B2
1 <= n + 1 by NAT_1:11;
then n + 1 in dom B1 by A6, FINSEQ_3:27;
then A7: ( B1 . (n + 1) = B1 /. (n + 1) & B2 . (n + 1) = B2 /. (n + 1) ) by A6, PARTFUN1:def 8;
A8: len (B1 | n) = n by A6, FINSEQ_1:80, NAT_1:11;
then A9: dom (B1 | n) = Seg n by FINSEQ_1:def 3;
A10: Sum (B1 | n) = Sum (B2 | n) by A5, A6, A8;
thus Sum B1 = (Sum (B1 | n)) + (B1 /. (n + 1)) by A6, A7, A8, A9, RLVECT_1:55
.= (Sum (B2 | n)) + (B2 /. (n + 1)) by A6, A7, A10, VECTSP_4:21
.= Sum B2 by A6, A7, A8, A9, RLVECT_1:55 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
then S₁[ len B1] ;
hence Sum B1 = Sum B2 by A1; :: thesis: verum