let X be RealUnitarySpace; for x being Point 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 Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
let x be Point 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 Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( 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 Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( 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 Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q
let q be FinSequence of REAL ; ( dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) implies x .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A2:
dom p = dom q
and
A3:
for i being Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)]
; x .|. ( the addF of X "**" p) = addreal "**" q
consider f being sequence of the carrier of X such that
A4:
f . 1 = p . 1
and
A5:
for n being Nat st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1)))
and
A6:
the addF of X "**" p = f . (len p)
by A1, FINSOP_1:1;
A7: Seg (len q) =
dom p
by A2, FINSEQ_1:def 3
.=
Seg (len p)
by FINSEQ_1:def 3
;
then A8:
len q = len p
by FINSEQ_1:6;
len q >= 1
by A1, A7, FINSEQ_1:6;
then consider g being sequence of REAL such that
A9:
g . 1 = q . 1
and
A10:
for n being Nat st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1)))
and
A11:
addreal "**" q = g . (len q)
by FINSOP_1:1;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len q implies g . $1 = the scalar of X . [x,(f . $1)] );
A12:
S1[ 0 ]
;
now for n being Nat st S1[n] & 1 <= n + 1 & n + 1 <= len q holds
g . (n + 1) = the scalar of X . [x,(f . (n + 1))]let n be
Nat;
( S1[n] & 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] )assume A13:
S1[
n]
;
( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] )now ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [x,(f . (n + 1))] )assume that A14:
1
<= n + 1
and A15:
n + 1
<= len q
;
g . (n + 1) = the scalar of X . [x,(f . (n + 1))]per cases
( n = 0 or n <> 0 )
;
suppose A17:
n <> 0
;
g . (n + 1) = the scalar of X . [x,(f . (n + 1))]then
0 < n
;
then A18:
0 + 1
<= n
by INT_1:7;
A19:
(n + 1) - 1
< (len q) - 0
by A15, XREAL_1:15;
A20:
n + 1
in Seg (len q)
by A14, A15, FINSEQ_1:1;
then A21:
n + 1
in dom q
by FINSEQ_1:def 3;
A22:
n + 1
in dom p
by A2, A20, FINSEQ_1:def 3;
A23:
n in NAT
by ORDINAL1:def 12;
dom f = NAT
by FUNCT_2:def 1;
then A24:
f . n in rng f
by FUNCT_1:3, A23;
rng f c= the
carrier of
X
by RELAT_1:def 19;
then reconsider z =
f . n as
Element of
X by A24;
A25:
p . (n + 1) in rng p
by A22, FUNCT_1:3;
rng p c= the
carrier of
X
by RELAT_1:def 19;
then reconsider y =
p . (n + 1) as
Element of
X by A25;
thus g . (n + 1) =
addreal . (
( the scalar of X . [x,(f . n)]),
(q . (n + 1)))
by A10, A13, A18, A19
.=
addreal . (
( the scalar of X . [x,(f . n)]),
( the scalar of X . [x,(p . (n + 1))]))
by A3, A21
.=
addreal . (
( the scalar of X . [x,(f . n)]),
(x .|. y))
by BHSP_1:def 1
.=
addreal . (
(x .|. z),
(x .|. y))
by BHSP_1:def 1
.=
(x .|. z) + (x .|. y)
by BINOP_2:def 9
.=
x .|. (z + y)
by BHSP_1:2
.=
the
scalar of
X . [x,( the addF of X . ((f . n),(p . (n + 1))))]
by BHSP_1:def 1
.=
the
scalar of
X . [x,(f . (n + 1))]
by A5, A8, A17, A19
;
verum end; end; hence
( 1
<= n + 1 &
n + 1
<= len q implies
g . (n + 1) = the
scalar of
X . [x,(f . (n + 1))] )
;
verum end;
then A26:
for n being Nat st S1[n] holds
S1[n + 1]
;
A27:
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A26);
1 <= len q
by A1, A7, FINSEQ_1:6;
then g . (len q) =
the scalar of X . [x,(f . (len q))]
by A27
.=
the scalar of X . [x,(f . (len p))]
by A7, FINSEQ_1:6
;
hence
x .|. ( the addF of X "**" p) = addreal "**" q
by A6, A11, BHSP_1:def 1; verum