let X be RealUnitarySpace; for L being linear-Functional of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let L be linear-Functional of X; for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; ( len p >= 1 implies for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q )
assume A1:
len p >= 1
; for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
consider f being Function of NAT, the carrier of X such that
A2:
f . 1 = p . 1
and
A3:
for n being Element of NAT st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1)))
and
A4:
the addF of X "**" p = f . (len p)
by A1, FINSOP_1:1;
let q be FinSequence of REAL ; ( dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) implies L . ( the addF of X "**" p) = addreal "**" q )
assume that
A5:
dom p = dom q
and
A6:
for i being Element of NAT st i in dom q holds
q . i = L . (p . i)
; L . ( the addF of X "**" p) = addreal "**" q
Seg (len q) =
dom p
by A5, FINSEQ_1:def 3
.=
Seg (len p)
by FINSEQ_1:def 3
;
then A7:
len q = len p
by FINSEQ_1:6;
then consider g being Function of NAT,REAL such that
A8:
g . 1 = q . 1
and
A9:
for n being Element of NAT st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1)))
and
A10:
addreal "**" q = g . (len q)
by A1, FINSOP_1:1;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len q implies g . $1 = L . (f . $1) );
A11:
now let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )assume A12:
S1[
n]
;
S1[n + 1]now A13:
n <= n + 1
by NAT_1:11;
assume that A14:
1
<= n + 1
and A15:
n + 1
<= len q
;
g . (n + 1) = L . (f . (n + 1))per cases
( n = 0 or n <> 0 )
;
suppose A17:
n <> 0
;
g . (n + 1) = L . (f . (n + 1))then A18:
0 + 1
<= n
by INT_1:7;
reconsider z =
f . n as
Element of
X ;
reconsider z1 =
z as
VECTOR of
X ;
A19:
n + 1
in dom q
by A14, A15, FINSEQ_3:25;
then
p . (n + 1) in rng p
by A5, FUNCT_1:3;
then reconsider y =
p . (n + 1) as
Element of
X ;
reconsider y1 =
y as
VECTOR of
X ;
set Lz =
L . z1;
set Ly =
L . y1;
A20:
(n + 1) - 1
< (len q) - 0
by A15, XREAL_1:15;
hence g . (n + 1) =
addreal . (
(g . n),
(q . (n + 1)))
by A9, A17
.=
addreal . (
(L . (f . n)),
(L . y))
by A6, A12, A15, A13, A18, A19, XXREAL_0:2
.=
(L . z1) + (L . y1)
by BINOP_2:def 9
.=
L . (z1 + y1)
by HAHNBAN:def 2
.=
L . (f . (n + 1))
by A3, A7, A17, A20
;
verum end; end; hence
S1[
n + 1]
;
verum end;
A21:
S1[ 0 ]
;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A21, A11);
hence
L . ( the addF of X "**" p) = addreal "**" q
by A1, A4, A7, A10; verum