let RS be RealLinearSpace; :: thesis: for X being Subset of RS
for g1, h1 being FinSequence of RS
for a1 being integer-valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
let X be Subset of RS; :: thesis: for g1, h1 being FinSequence of RS
for a1 being integer-valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X
defpred S₁[ Nat] means for g, h being FinSequence of RS
for s being integer-valued FinSequence st rng g c= X & len g = $1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin X;
P0: S₁[ 0 ]

proof

let g, h be FinSequence of RS; :: thesis: for s being integer-valued FinSequence st rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin X
let s be integer-valued FinSequence; :: thesis: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin X )
set x = Sum h;
assume AS1: ( rng g c= X & len g = 0 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; :: thesis: Sum h in Z_Lin X
Sum h = Sum (<*> the carrier of RS) by AS1, FINSEQ_1:28
.= 0. RS by RLVECT_1:60 ;
hence Sum h in Z_Lin X by LM030; :: thesis: verum

end;

P1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume P10: S₁[n] ; :: thesis: S₁[n + 1]

now

let g, h be FinSequence of RS; :: thesis: for s being integer-valued FinSequence
for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
x in Z_Lin X
let s be integer-valued FinSequence; :: thesis: for x being set st x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
x in Z_Lin X
let x be set ; :: thesis: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies x in Z_Lin X )
assume AS1: ( x = Sum h & rng g c= X & len g = n + 1 & len g = len h & len g = len s & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; :: thesis: x in Z_Lin X
reconsider gn = g | n as FinSequence of RS ;
reconsider hn = h | n as FinSequence of RS ;
reconsider sn = s | n as real-valued FinSequence ;
( rng gn c= X & len gn = n & len gn = len hn & len gn = len sn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ) )

proof

rng gn c= rng g by RELAT_1:99;
then B0: rng gn c= X by AS1, XBOOLE_1:1;
B1: n <= len g by AS1, NAT_1:11;
B3: n <= len h by AS1, NAT_1:11;
B4: len hn = n by AS1, NAT_1:11, FINSEQ_1:80;
B5: len sn = n by AS1, NAT_1:11, FINSEQ_1:80;
for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)

proof

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)

hence for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i)

then C1: n >= 1 by NAT_1:14;
let i be Nat; :: thesis: ( i in Seg (len gn) implies hn /. i = (sn . i) * (gn /. i) )
assume i in Seg (len gn) ; :: thesis: hn /. i = (sn . i) * (gn /. i)
then C2: i in Seg n by AS1, NAT_1:11, FINSEQ_1:80;
n in Seg (len g) by B1, C1, FINSEQ_1:3;
then n in dom g by FINSEQ_1:def 3;
then C4: gn /. i = g /. i by C2, FINSEQ_4:86;
n in Seg (len h) by B3, C1, FINSEQ_1:3;
then n in dom h by FINSEQ_1:def 3;
then C5: hn /. i = h /. i by C2, FINSEQ_4:86;
i <= n by C2, FINSEQ_1:3;
then sn . i = s . i by FINSEQ_3:121;
hence hn /. i = (sn . i) * (gn /. i) by AS1, C2, C4, C5, FINSEQ_2:9; :: thesis: verum

end;

end;

end;

hence ( rng gn c= X & len gn = n & len gn = len hn & len gn = len sn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ) ) by B0, B4, B5, AS1, NAT_1:11, FINSEQ_1:80; :: thesis: verum

end;

then Q3: Sum hn in Z_Lin X by P10;
Q4: n + 1 in Seg (len g) by AS1, FINSEQ_1:6;
Q5: h /. (n + 1) = (s . (n + 1)) * (g /. (n + 1)) by AS1, FINSEQ_1:6;
Q6: h = hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*> by AS1, Q5, FINSEQ_5:24;
Q7: n + 1 in dom g by Q4, FINSEQ_1:def 3;
then g /. (n + 1) = g . (n + 1) by PARTFUN1:def 8;
then g /. (n + 1) in rng g by Q7, FUNCT_1:12;
then g /. (n + 1) in Z_Lin X by AS1, Th18;
then Q8: (s . (n + 1)) * (g /. (n + 1)) in Z_Lin X by LM020;
Sum h = (Sum hn) + (Sum <*((s . (n + 1)) * (g /. (n + 1)))*>) by Q6, RLVECT_1:58
.= (Sum hn) + ((s . (n + 1)) * (g /. (n + 1))) by RLVECT_1:61 ;
hence x in Z_Lin X by AS1, Q3, Q8, LM010; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
hence for g1, h1 being FinSequence of RS
for a1 being integer-valued FinSequence st rng g1 c= X & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) holds
Sum h1 in Z_Lin X ; :: thesis: verum