let RS be RealLinearSpace; :: thesis: for f being non empty FinSequence of RS
for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
let f be non empty FinSequence of RS; :: thesis: for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
( 1 <= 1 & 1 <= len f ) by FINSEQ_1:20;
then 1 in Seg (len f) ;
then A1: f /. 1 in Z_Lin f by Th30;
reconsider z0 = 0 as Element of INT by NUMBERS:17;
reconsider z1 = 1 as Element of INT by NUMBERS:17;
(z0 * (f /. 1)) + (z0 * (f /. 1)) in Z_Lin f by Th27, A1;
then (z0 * (f /. 1)) + (0. RS) in Z_Lin f by RLVECT_1:10;
then A2: (0. RS) + (0. RS) in Z_Lin f by RLVECT_1:10;
defpred S₁[ Nat] means for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = $1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f;
A3: S₁[ 0 ]

proof

let g, h be FinSequence of RS; :: thesis: for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f
let s be INT -valued FinSequence; :: thesis: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) implies Sum h in Z_Lin f )
assume A4: ( rng g c= Z_Lin f & len g = 0 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) ) ; :: thesis: Sum h in Z_Lin f
Sum h = Sum (<*> the carrier of RS) by A4, FINSEQ_1:20
.= 0. RS by RLVECT_1:43 ;
hence Sum h in Z_Lin f by A2, RLVECT_1:4; :: thesis: verum

end;

A5: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = n + 1 & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f

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

proof

A9: rng gn c= rng g by RELAT_1:70;
A10: n <= len g by A7, NAT_1:11;
A11: n <= len h by A7, NAT_1:11;
A12: len hn = n by A7, FINSEQ_1:59, NAT_1:11;
A13: len sn = n by A7, FINSEQ_1:59, NAT_1:11;
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 A14: 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 A15: i in Seg n by A7, FINSEQ_1:59, NAT_1:11;
n in Seg (len g) by A10, A14;
then n in dom g by FINSEQ_1:def 3;
then A16: gn /. i = g /. i by A15, FINSEQ_4:71;
n in Seg (len h) by A11, A14;
then n in dom h by FINSEQ_1:def 3;
then A17: hn /. i = h /. i by A15, FINSEQ_4:71;
i <= n by A15, FINSEQ_1:1;
then sn . i = s . i by FINSEQ_3:112;
hence hn /. i = (sn . i) * (gn /. i) by A7, A15, A16, A17, FINSEQ_2:8; :: thesis: verum

end;

end;

end;

hence ( rng gn c= Z_Lin f & len gn = n & len gn = len sn & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (sn . i) * (gn /. i) ) ) by A9, A10, A12, A13, A7, FINSEQ_1:59; :: thesis: verum

end;

A18: Sum hn in Z_Lin f by A8, A6;
A19: n + 1 in Seg (len g) by A7, FINSEQ_1:4;
A20: h /. (n + 1) = (s . (n + 1)) * (g /. (n + 1)) by A7, FINSEQ_1:4;
A21: h = hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*> by A7, A20, FINSEQ_5:21;
A22: n + 1 in dom g by A19, FINSEQ_1:def 3;
then g /. (n + 1) = g . (n + 1) by PARTFUN1:def 6;
then g /. (n + 1) in rng g by A22, FUNCT_1:3;
then ((z1 * (s . (n + 1))) * (g /. (n + 1))) + (z0 * (g /. (n + 1))) in Z_Lin f by A7, Th27;
then ((z1 * (s . (n + 1))) * (g /. (n + 1))) + (0. RS) in Z_Lin f by RLVECT_1:10;
then (z1 * (s . (n + 1))) * (g /. (n + 1)) in Z_Lin f by RLVECT_1:4;
then (z1 * (Sum hn)) + (z1 * ((s . (n + 1)) * (g /. (n + 1)))) in Z_Lin f by A18, Th27;
then A23: (z1 * (Sum hn)) + ((s . (n + 1)) * (g /. (n + 1))) in Z_Lin f by RLVECT_1:def 8;
Sum h = (Sum hn) + (Sum <*((s . (n + 1)) * (g /. (n + 1)))*>) by A21, RLVECT_1:41
.= (Sum hn) + ((s . (n + 1)) * (g /. (n + 1))) by RLVECT_1:44 ;
hence Sum h in Z_Lin f by A23, RLVECT_1:def 8; :: thesis: verum

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A5);
hence for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f ; :: thesis: verum