let V be RealLinearSpace; 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; 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 S1[ 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:
S1[ 0 ]
A3:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A4:
S1[
n]
;
S1[n + 1]now 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 Alet x be
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 Alet g1,
h1 be
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 Alet a1 be
INT -valued FinSequence;
( 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) ) )
;
Sum h1 in Z_Lin Areconsider 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
;
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;
( i in Seg (len gn) implies hn /. i = (an . i) * (gn /. i) )assume
i in Seg (len gn)
;
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;
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;
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;
verum end; hence
S1[
n + 1]
;
verum end;
for n being Nat holds S1[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
; verum