defpred S₁[ Nat] means for X being RealLinearSpace-Sequence
for d being FinSequence of NAT st len X = $1 & len d = len X & ( for i being Element of dom X holds
( X . i is finite-dimensional & d . i = dim (X . i) ) ) holds
( product X is finite-dimensional & dim (product X) = Sum d );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:

per cases ;

suppose A4: n = 0 ; :: thesis:

let X be RealLinearSpace-Sequence; :: thesis:
let d be FinSequence of NAT ; :: thesis:
assume A5: ( len X = n + 1 & len d = len X & ( for i being Element of dom X holds
( X . i is finite-dimensional & d . i = dim (X . i) ) ) ) ; :: thesis:
A6: 1 in Seg (n + 1) by A4;
then A7: 1 in dom X by A5, FINSEQ_1:def 3;
reconsider i1 = 1 as Element of dom X by A5, A6, FINSEQ_1:def 3;
X . 1 in rng X by A7, FUNCT_1:3;
then reconsider X1 = X . 1 as RealLinearSpace by PRVECT_2:def 3;
A8: X = <*X1*> by A4, A5, FINSEQ_1:40;
A9: d = <*(d . 1)*> by A4, A5, FINSEQ_1:40;
X . i1 = X1 ;
then A10: ( X1 is finite-dimensional & d . i1 = dim X1 ) by A5;
Sum d = d . i1 by A9, RVSUM_1:73
.= dim X1 by A5 ;
hence ( product X is finite-dimensional & dim (product X) = Sum d ) by A8, A10, Th27; :: thesis:

end;

suppose A11: n <> 0 ; :: thesis:

let X be RealLinearSpace-Sequence; :: thesis:
let d be FinSequence of NAT ; :: thesis:
assume A12: ( len X = n + 1 & len d = len X & ( for i being Element of dom X holds
( X . i is finite-dimensional & d . i = dim (X . i) ) ) ) ; :: thesis:
set Y = X | n;
set e = d | n;
A13: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A14: n + 1 in dom X by A12, FINSEQ_1:def 3;
A15: n <= n + 1 by NAT_1:11;
A16: len (X | n) = n by A12, FINSEQ_1:59, NAT_1:11;
for S being set st S in rng (X | n) holds
S is RealLinearSpace

proof

let S be set ; :: thesis:
assume S in rng (X | n) ; :: thesis:
then consider x being object such that
A17: ( x in dom (X | n) & S = (X | n) . x ) by FUNCT_1:def 3;
x in Seg n by A16, A17, FINSEQ_1:def 3;
then x in Seg (n + 1) by A15, FINSEQ_1:5, TARSKI:def 3;
then x in dom X by FINSEQ_1:def 3, A12;
then X . x in rng X by FUNCT_1:3;
then X . x is RealLinearSpace by PRVECT_2:def 3;
hence S is RealLinearSpace by A17, FUNCT_1:47; :: thesis:

end;

then reconsider Y = X | n as RealLinearSpace-Sequence by A11, PRVECT_2:def 3;
reconsider e = d | n as FinSequence of NAT ;
A18: len e = n by A12, FINSEQ_1:59, NAT_1:11;
A19: for i being Element of dom Y holds
( Y . i is finite-dimensional & e . i = dim (Y . i) )

proof

let i be Element of dom Y; :: thesis:
i in dom Y ;
then A20: i in Seg (len Y) by FINSEQ_1:def 3;
i in Seg (n + 1) by A15, A16, A20, FINSEQ_1:5, TARSKI:def 3;
then reconsider i0 = i as Element of dom X by A12, FINSEQ_1:def 3;
A21: i in dom e by A16, A18, A20, FINSEQ_1:def 3;
X . i0 is finite-dimensional by A12;
hence Y . i is finite-dimensional by FUNCT_1:47; :: thesis:
thus e . i = d . i by FUNCT_1:47, A21
.= dim (X . i0) by A12
.= dim (Y . i) by FUNCT_1:47 ; :: thesis:

end;

then A22: ( product Y is finite-dimensional & dim (product Y) = Sum e ) by A3, A16, A18;
reconsider m = n + 1 as Element of dom X by A12, A13, FINSEQ_1:def 3;
X . m is RealLinearSpace ;
then reconsider Xm = X . (n + 1) as RealLinearSpace ;
reconsider Xm = Xm as finite-dimensional RealLinearSpace by A12, A14;
A23: ( [:(product Y),Xm:] is finite-dimensional & dim [:(product Y),Xm:] = (dim (product Y)) + (dim Xm) ) by A22, Th26;
consider I being Function of [:(product Y),Xm:],(product (Y ^ <*Xm*>)) such that
A24: ( I is one-to-one & I is onto ) and
for v being Point of (product Y)
for w being Point of Xm ex v1, w1 being FinSequence st
( v = v1 & <*w*> = w1 & I . (v,w) = v1 ^ w1 ) and
A25: for v, w being Point of [:(product Y),Xm:] holds I . (v + w) = (I . v) + (I . w) and
A26: for v being Point of [:(product Y),Xm:]
for r being Element of REAL holds I . (r * v) = r * (I . v) and
I . (0. [:(product Y),Xm:]) = 0. (product (Y ^ <*Xm*>)) by PRVECT_3:22;
A27: I is additive by A25;
for v being VECTOR of [:(product Y),Xm:]
for r being Real holds I . (r * v) = r * (I . v)

proof

let v be VECTOR of [:(product Y),Xm:]; :: thesis:
let r be Real; :: thesis:
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus I . (r * v) = r0 * (I . v) by A26
.= r * (I . v) ; :: thesis:

end;

then A28: I is homogeneous by LOPBAN_1:def 5;
A29: ( product (Y ^ <*Xm*>) is finite-dimensional & dim (product (Y ^ <*Xm*>)) = dim [:(product Y),Xm:] ) by A23, A24, A27, A28, REAL_NS2:88;
A30: e ^ <*(d . (n + 1))*> = d by A12, FINSEQ_3:55;
dim [:(product Y),Xm:] = (dim (product Y)) + (dim Xm) by A22, Th26
.= (Sum e) + (dim Xm) by A3, A16, A18, A19
.= (Sum e) + (d . m) by A12
.= Sum d by A30, RVSUM_1:74 ;
hence ( product X is finite-dimensional & dim (product X) = Sum d ) by A12, A29, FINSEQ_3:55; :: thesis:

end;

end;

end;

A31: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let X be RealLinearSpace-Sequence; :: thesis:
let d be FinSequence of NAT ; :: thesis:
assume ( len d = len X & ( for i being Element of dom X holds
( X . i is finite-dimensional & d . i = dim (X . i) ) ) ) ; :: thesis:
hence ( product X is finite-dimensional & dim (product X) = Sum d ) by A31; :: thesis: