let X be RealUnitarySpace; for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) 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 . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; ( len p >= 1 & ( for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) 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 . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A1:
len p >= 1
and
A2:
for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0
; 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 . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
A3:
1 in dom p
by A1, FINSEQ_3:25;
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 . [(p . i),(p . i)] ) implies ( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q )
assume that
A4:
dom p = dom q
and
A5:
for i being Nat st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)]
; ( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
consider f being sequence of the carrier of X such that
A6:
f . 1 = p . 1
and
A7:
for n being Nat st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1)))
and
A8:
the addF of X "**" p = f . (len p)
by A1, FINSOP_1:1;
A9:
( the addF of X "**" p) .|. ( the addF of X "**" p) = the scalar of X . [(f . (len p)),(f . (len p))]
by A8, BHSP_1:def 1;
A10: Seg (len q) =
dom p
by A4, FINSEQ_1:def 3
.=
Seg (len p)
by FINSEQ_1:def 3
;
then A11:
len q = len p
by FINSEQ_1:6;
len q >= 1
by A1, A10, FINSEQ_1:6;
then consider g being sequence of REAL such that
A12:
g . 1 = q . 1
and
A13:
for n being Nat st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1)))
and
A14:
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 . [(f . $1),(f . $1)] );
A15:
S1[ 0 ]
;
now for n being Nat st ( 1 <= n & n <= len q implies g . n = the scalar of X . [(f . n),(f . n)] ) & 1 <= n + 1 & n + 1 <= len q holds
g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]let n be
Nat;
( ( 1 <= n & n <= len q implies g . n = the scalar of X . [(f . n),(f . n)] ) & 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] )assume A16:
( 1
<= n &
n <= len q implies
g . n = the
scalar of
X . [(f . n),(f . n)] )
;
( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] )now ( 1 <= n + 1 & n + 1 <= len q implies g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))] )assume that A17:
1
<= n + 1
and A18:
n + 1
<= len q
;
g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]A19:
n <= n + 1
by NAT_1:11;
per cases
( n = 0 or n <> 0 )
;
suppose A21:
n <> 0
;
g . (n + 1) = the scalar of X . [(f . (n + 1)),(f . (n + 1))]then
0 < n
;
then A22:
0 + 1
<= n
by INT_1:7;
A23:
n <= len p
by A11, A18, A19, XXREAL_0:2;
A24:
(n + 1) - 1
< (len q) - 0
by A18, XREAL_1:15;
then A25:
n < len p
by A10, FINSEQ_1:6;
A26:
n + 1
in Seg (len q)
by A17, A18, FINSEQ_1:1;
then A27:
n + 1
in dom q
by FINSEQ_1:def 3;
A28:
n + 1
in dom p
by A4, A26, FINSEQ_1:def 3;
A29:
n in NAT
by ORDINAL1:def 12;
A30:
dom f = NAT
by FUNCT_2:def 1;
then A31:
f . n in rng f
by FUNCT_1:3, A29;
rng f c= the
carrier of
X
by RELAT_1:def 19;
then reconsider z =
f . n as
Element of
X by A31;
A32:
p . (n + 1) in rng p
by A28, 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 A32;
for
i being
Nat st 1
<= i &
i <= n holds
the
scalar of
X . [(f . i),y] = 0
proof
let i be
Nat;
( 1 <= i & i <= n implies the scalar of X . [(f . i),y] = 0 )
defpred S2[
Nat]
means ( 1
<= $1 & $1
<= n implies the
scalar of
X . [(f . $1),y] = 0 );
A33:
S2[
0 ]
;
A34:
for
i being
Nat st
S2[
i] holds
S2[
i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A35:
S2[
i]
;
S2[i + 1]
A36:
1
<> n + 1
by A21;
assume that A37:
1
<= i + 1
and A38:
i + 1
<= n
;
the scalar of X . [(f . (i + 1)),y] = 0
i + 1
<= len p
by A23, A38, XXREAL_0:2;
then A39:
i + 1
in dom p
by A37, FINSEQ_3:25;
A40:
i in NAT
by ORDINAL1:def 12;
per cases
( i = 0 or i <> 0 )
;
suppose A41:
i <> 0
;
the scalar of X . [(f . (i + 1)),y] = 0 A42:
f . i in rng f
by A30, FUNCT_1:3, A40;
rng f c= the
carrier of
X
by RELAT_1:def 19;
then reconsider s =
f . i as
Element of
X by A42;
A43:
i + 1
<= len p
by A23, A38, XXREAL_0:2;
then
i + 1
in dom p
by A37, FINSEQ_3:25;
then A44:
p . (i + 1) in rng p
by FUNCT_1:3;
rng p c= the
carrier of
X
by RELAT_1:def 19;
then reconsider t =
p . (i + 1) as
Element of
X by A44;
A45:
(i + 1) - 1
< (len p) - 0
by A43, XREAL_1:15;
0 < i
by A41;
then A46:
0 + 1
<= i
by INT_1:7;
i < i + 1
by XREAL_1:29;
then A47:
s .|. y = 0
by A35, A38, A46, BHSP_1:def 1, XXREAL_0:2;
A48:
(i + 1) + 0 < n + 1
by A38, XREAL_1:8;
the
scalar of
X . [(f . (i + 1)),y] =
the
scalar of
X . [(s + t),y]
by A7, A41, A45
.=
(s + t) .|. y
by BHSP_1:def 1
.=
0 + (t .|. y)
by A47, BHSP_1:2
.=
the
scalar of
X . [t,y]
by BHSP_1:def 1
.=
0
by A2, A28, A39, A48
;
hence
the
scalar of
X . [(f . (i + 1)),y] = 0
;
verum end;
end;
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A33, A34);
hence
( 1
<= i &
i <= n implies the
scalar of
X . [(f . i),y] = 0 )
;
verum
end; then A49:
0 =
the
scalar of
X . [z,y]
by A22
.=
z .|. y
by BHSP_1:def 1
;
thus g . (n + 1) =
addreal . (
( the scalar of X . [(f . n),(f . n)]),
(q . (n + 1)))
by A13, A16, A22, A24
.=
addreal . (
( the scalar of X . [(f . n),(f . n)]),
( the scalar of X . [(p . (n + 1)),(p . (n + 1))]))
by A5, A27
.=
addreal . (
( the scalar of X . [(f . n),(f . n)]),
(y .|. y))
by BHSP_1:def 1
.=
addreal . (
(z .|. z),
(y .|. y))
by BHSP_1:def 1
.=
(((z .|. z) + (z .|. y)) + (y .|. z)) + (y .|. y)
by A49, BINOP_2:def 9
.=
((z .|. (z + y)) + (y .|. z)) + (y .|. y)
by BHSP_1:2
.=
(z .|. (z + y)) + ((y .|. z) + (y .|. y))
.=
(z .|. (z + y)) + (y .|. (z + y))
by BHSP_1:2
.=
(z + y) .|. (z + y)
by BHSP_1:2
.=
the
scalar of
X . [( the addF of X . ((f . n),(p . (n + 1)))),(z + y)]
by BHSP_1:def 1
.=
the
scalar of
X . [( the addF of X . ((f . n),(p . (n + 1)))),(f . (n + 1))]
by A7, A21, A25
.=
the
scalar of
X . [(f . (n + 1)),(f . (n + 1))]
by A7, A21, A25
;
verum end; end; hence
( 1
<= n + 1 &
n + 1
<= len q implies
g . (n + 1) = the
scalar of
X . [(f . (n + 1)),(f . (n + 1))] )
;
verum end;
then A50:
for n being Nat st S1[n] holds
S1[n + 1]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A15, A50);
hence
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q
by A1, A9, A11, A14; verum