let V be RealLinearSpace; :: thesis: for A being Subset of V
for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & 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
x in Z_Lin A
let A be Subset of V; :: thesis: for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & 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
x in Z_Lin A
reconsider z0 = 0 as Element of INT by NUMBERS:17;
reconsider z1 = 1 as Element of INT by NUMBERS:17;
defpred S₁[ Nat] means for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = $1 & 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
x in Z_Lin A;
A1: S₁[ 0 ]

proof

let x be set ; :: thesis: for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & 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
x in Z_Lin A
let g1, h1 be FinSequence of V; :: thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & 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
x in Z_Lin A
let a1 be INT -valued FinSequence; :: thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & 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) ) implies x in Z_Lin A )
assume A2: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = 0 & 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) ) ) ; :: thesis: x in Z_Lin A
Sum h1 = Sum (<*> the carrier of V) by A2, FINSEQ_1:20
.= 0. V by RLVECT_1:43 ;
hence x in Z_Lin A by A2, Th11; :: thesis: verum

end;

A3: 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 A4: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & 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 A

let x be set ; :: thesis: for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & 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 A
let g1, h1 be FinSequence of V; :: thesis: for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & 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 A
let a1 be INT -valued FinSequence; :: thesis: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & 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) ) implies Sum h1 in Z_Lin A )
assume A5: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = n + 1 & 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) ) ) ; :: thesis: Sum h1 in Z_Lin A
reconsider gn = g1 | n as FinSequence of V ;
reconsider hn = h1 | n as FinSequence of V ;
reconsider an = a1 | n as INT -valued FinSequence ;
A6: ( rng gn c= Z_Lin A & len gn = n & len gn = len an & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i) ) )

proof

A7: rng gn c= rng g1 by RELAT_1:70;
A8: n <= len g1 by A5, NAT_1:11;
A9: n <= len h1 by A5, NAT_1:11;
A10: len hn = n by A5, FINSEQ_1:59, NAT_1:11;
A11: len an = n by A5, FINSEQ_1:59, NAT_1:11;
for i being Nat st i in Seg (len gn) holds
hn /. i = (an . 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 = (an . i) * (gn /. i)

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

end;

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

then A12: n >= 1 by NAT_1:14;
let i be Nat; :: thesis: ( i in Seg (len gn) implies hn /. i = (an . i) * (gn /. i) )
assume i in Seg (len gn) ; :: thesis: hn /. i = (an . i) * (gn /. i)
then A13: i in Seg n by A5, FINSEQ_1:59, NAT_1:11;
n in Seg (len g1) by A8, A12;
then n in dom g1 by FINSEQ_1:def 3;
then A14: gn /. i = g1 /. i by A13, FINSEQ_4:71;
n in Seg (len h1) by A9, A12;
then n in dom h1 by FINSEQ_1:def 3;
then A15: hn /. i = h1 /. i by A13, FINSEQ_4:71;
i <= n by A13, FINSEQ_1:1;
then an . i = a1 . i by FINSEQ_3:112;
hence hn /. i = (an . i) * (gn /. i) by A5, A13, A14, A15, FINSEQ_2:8; :: thesis: verum

end;

end;

end;

hence ( rng gn c= Z_Lin A & len gn = n & len gn = len an & len gn = len hn & ( for i being Nat st i in Seg (len gn) holds
hn /. i = (an . i) * (gn /. i) ) ) by A5, A7, A8, A10, A11, FINSEQ_1:59; :: thesis: verum

end;

A16: n + 1 in Seg (len g1) by A5, FINSEQ_1:4;
A17: h1 /. (n + 1) = (a1 . (n + 1)) * (g1 /. (n + 1)) by A5, FINSEQ_1:4;
A18: h1 = hn ^ <*((a1 . (n + 1)) * (g1 /. (n + 1)))*> by A5, A17, FINSEQ_5:21;
A19: n + 1 in dom g1 by A16, FINSEQ_1:def 3;
then g1 /. (n + 1) = g1 . (n + 1) by PARTFUN1:def 6;
then g1 /. (n + 1) in rng g1 by A19, FUNCT_1:3;
then ( (z1 * (a1 . (n + 1))) * (g1 /. (n + 1)) in Z_Lin A & z0 * (g1 /. (n + 1)) in Z_Lin A ) by A5, Th10;
then ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + (z0 * (g1 /. (n + 1))) in Z_Lin A by Th9;
then ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + (0. V) in Z_Lin A by RLVECT_1:10;
then A20: (z1 * (a1 . (n + 1))) * (g1 /. (n + 1)) in Z_Lin A by RLVECT_1:4;
z1 * (Sum hn) in Z_Lin A by A4, A6, Th10;
then A21: (z1 * (Sum hn)) + ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) in Z_Lin A by A20, Th9;
Sum h1 = (Sum hn) + (Sum <*((a1 . (n + 1)) * (g1 /. (n + 1)))*>) by A18, RLVECT_1:41
.= (Sum hn) + ((a1 . (n + 1)) * (g1 /. (n + 1))) by RLVECT_1:44 ;
hence Sum h1 in Z_Lin A by A21, 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(A1, A3);
hence for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin A & 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
x in Z_Lin A ; :: thesis: verum