let X be RealNormSpace; :: thesis: for x being Point of X
for M being non empty Subspace of X
for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
let x be Point of X; :: thesis: for M being non empty Subspace of X
for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
let M be non empty Subspace of X; :: thesis: for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
defpred S₁[ Nat] means for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len F = $1 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } ;
A1: S₁[ 0 ]

proof

let F, K be FinSequence of the carrier of X; :: thesis: for G being FinSequence of REAL st len F = 0 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
let G be FinSequence of REAL ; :: thesis: ( len F = 0 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) implies Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } )
assume A2: ( len F = 0 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) ) ; :: thesis: Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
K = <*> the carrier of X by A2;
then A3: Sum K = 0. X by RLVECT_1:43;
A4: 0. X in M by RLSUB_1:17;
(0 * x) + (0. X) = 0. X by RLVECT_1:10;
hence Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } by A3, A4; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let F, K be FinSequence of the carrier of X; :: thesis: for G being FinSequence of REAL st len F = k + 1 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
let G be FinSequence of REAL ; :: thesis: ( len F = k + 1 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) implies Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } )
assume A7: ( len F = k + 1 & len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) ) ; :: thesis: Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }
reconsider F1 = F | k, K1 = K | k as FinSequence of the carrier of X ;
reconsider G1 = G | k as FinSequence of REAL ;
A8: ( len F1 = k & len K1 = k & len G1 = k ) by FINSEQ_1:59, A7, NAT_1:11;
A9: dom F = Seg (k + 1) by A7, FINSEQ_1:def 3;
A10: dom F1 = Seg (len F1) by FINSEQ_1:def 3
.= Seg k by FINSEQ_1:59, A7, NAT_1:11 ;
A11: dom K = Seg (k + 1) by A7, FINSEQ_1:def 3;
A12: dom K1 = Seg (len K1) by FINSEQ_1:def 3
.= Seg k by FINSEQ_1:59, A7, NAT_1:11 ;
A13: dom G = Seg (k + 1) by A7, FINSEQ_1:def 3;
A14: dom G1 = Seg (len G1) by FINSEQ_1:def 3
.= Seg k by FINSEQ_1:59, A7, NAT_1:11 ;
A15: for i being Nat st i in dom F1 holds
F1 . i in x + M

proof

let i be Nat; :: thesis: ( i in dom F1 implies F1 . i in x + M )
assume A16P: i in dom F1 ; :: thesis: F1 . i in x + M
then A17: ( 1 <= i & i <= k ) by A10, FINSEQ_1:1;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A17, XXREAL_0:2;
then A18P: i in Seg (k + 1) by A17;
F1 . i = F . i by A16P, A10, FUNCT_1:49;
hence F1 . i in x + M by A18P, A9, A7; :: thesis: verum

end;

A19: for i being Nat st i in dom K1 holds
K1 . i = (G1 /. i) * (F1 /. i)

proof

let i be Nat; :: thesis: ( i in dom K1 implies K1 . i = (G1 /. i) * (F1 /. i) )
assume A20P: i in dom K1 ; :: thesis: K1 . i = (G1 /. i) * (F1 /. i)
then A22: ( 1 <= i & i <= k ) by A12, FINSEQ_1:1;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A22, XXREAL_0:2;
then A23: i in Seg (k + 1) by A22;
then A24: K . i = (G /. i) * (F /. i) by A7, A11;
A25: G /. i = G . i by PARTFUN1:def 6, A23, A13
.= G1 . i by FUNCT_1:49, A20P, A12
.= G1 /. i by PARTFUN1:def 6, A20P, A12, A14 ;
F /. i = F . i by PARTFUN1:def 6, A23, A9
.= F1 . i by FUNCT_1:49, A20P, A12
.= F1 /. i by PARTFUN1:def 6, A20P, A12, A10 ;
hence K1 . i = (G1 /. i) * (F1 /. i) by A20P, A12, FUNCT_1:49, A24, A25; :: thesis: verum

end;

Sum K1 in { ((a * x) + m) where a is Real, m is Point of X : m in M } by A6, A8, A15, A19;
then consider a being Real, m1 being Point of X such that
A26: ( Sum K1 = (a * x) + m1 & m1 in M ) ;
F . (k + 1) in x + M by A7, FINSEQ_1:4, A9;
then F /. (k + 1) in x + M by FINSEQ_1:4, A9, PARTFUN1:def 6;
then consider m being Point of X such that
A28: ( F /. (k + 1) = x + m & m in M ) ;
A30: K . (len K) = (G /. (k + 1)) * (F /. (k + 1)) by A7, A11, FINSEQ_1:4;
set b = G /. (k + 1);
A31: K . (len K) = ((G /. (k + 1)) * x) + ((G /. (k + 1)) * m) by RLVECT_1:def 5, A30, A28;
A32: (G /. (k + 1)) * m in M by A28, RLSUB_1:21;
dom K1 = Seg (len K1) by FINSEQ_1:def 3
.= Seg k by FINSEQ_1:59, A7, NAT_1:11 ;
then A33: Sum K = (Sum K1) + (((G /. (k + 1)) * x) + ((G /. (k + 1)) * m)) by A7, A8, A31, RLVECT_1:38
.= (((a * x) + m1) + ((G /. (k + 1)) * x)) + ((G /. (k + 1)) * m) by RLVECT_1:def 3, A26
.= (((a * x) + ((G /. (k + 1)) * x)) + m1) + ((G /. (k + 1)) * m) by RLVECT_1:def 3
.= (((a + (G /. (k + 1))) * x) + m1) + ((G /. (k + 1)) * m) by RLVECT_1:def 6
.= ((a + (G /. (k + 1))) * x) + (m1 + ((G /. (k + 1)) * m)) by RLVECT_1:def 3 ;
m1 + ((G /. (k + 1)) * m) in M by A32, A26, RLSUB_1:20;
hence Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } by A33; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
hence for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M } ; :: thesis: verum