let X be RealNormSpace-Sequence; for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)
let Y be RealNormSpace; for g being MultilinearOperator of X,Y
for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)
let g be MultilinearOperator of X,Y; for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)
let a be FinSequence of REAL ; ( dom a = dom X implies for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t) )
assume A1:
dom a = dom X
; for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)
A4:
dom (carr X) = dom X
by LemmaX;
A5:
product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #)
by PRVECT_2:6;
defpred S1[ Nat] means for t, t1 being Point of (product X)
for b being FinSequence of REAL st b = a | $1 & $1 <= len a & ( for i being Element of dom X holds
( ( i in Seg $1 implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg $1 implies t1 . i = t . i ) ) ) holds
g . t1 = (Product b) * (g . t);
A6:
S1[ 0 ]
A15:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A16:
S1[
k]
;
S1[k + 1]
let t,
t1 be
Point of
(product X);
for b being FinSequence of REAL st b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg (k + 1) implies t1 . i = t . i ) ) ) holds
g . t1 = (Product b) * (g . t)let b be
FinSequence of
REAL ;
( b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg (k + 1) implies t1 . i = t . i ) ) ) implies g . t1 = (Product b) * (g . t) )
assume A17:
(
b = a | (k + 1) &
k + 1
<= len a & ( for
i being
Element of
dom X holds
( (
i in Seg (k + 1) implies
t1 . i = (a /. i) * (t . i) ) & ( not
i in Seg (k + 1) implies
t1 . i = t . i ) ) ) )
;
g . t1 = (Product b) * (g . t)
reconsider b2 =
a | k as
FinSequence of
REAL ;
A18:
k <= k + 1
by NAT_1:11;
( 1
<= k + 1 &
k + 1
<= len a )
by A17, NAT_1:11;
then B19:
k + 1
in Seg (len a)
;
then A20:
k + 1
in dom a
by FINSEQ_1:def 3;
A22:
b2 = b | k
by A17, FINSEQ_1:82, NAT_1:11;
A23:
b =
b2 ^ <*(b . (k + 1))*>
by A17, A22, FINSEQ_1:59, FINSEQ_3:55
.=
b2 ^ <*(a . (k + 1))*>
by A17, FINSEQ_1:4, FUNCT_1:49
.=
b2 ^ <*(a /. (k + 1))*>
by A20, PARTFUN1:def 6
;
defpred S2[
object ]
means $1
in Seg k;
deffunc H1(
Element of
dom X)
-> Element of the
carrier of
(X . $1) =
(a /. $1) * (t . $1);
deffunc H2(
Element of
dom X)
-> Point of
(X . $1) =
t . $1;
consider s2 being
Function such that A25:
(
dom s2 = dom X & ( for
i being
Element of
dom X holds
( (
S2[
i] implies
s2 . i = H1(
i) ) & ( not
S2[
i] implies
s2 . i = H2(
i) ) ) ) )
from PARTFUN1:sch 4();
for
y being
object st
y in dom (carr X) holds
s2 . y in (carr X) . y
then reconsider s2 =
s2 as
Element of
product (carr X) by A4, A25, CARD_3:def 5;
reconsider t2 =
s2 as
Point of
(product X) by A5;
reconsider k1 =
k + 1 as
Element of
dom X by A1, B19, FINSEQ_1:def 3;
k + 0 < k + 1
by XREAL_1:8;
then
not
k1 in Seg k
by FINSEQ_1:1;
then A29:
s2 . k1 = t . k1
by A25;
A30:
g * (reproj (k1,t2)) is
LinearOperator of
(X . k1),
Y
by Def3;
set RK =
(reproj (k1,t2)) . ((a /. k1) * (t . k1));
A31:
ex
g being
Function st
(
t1 = g &
dom g = dom (carr X) & ( for
y being
object st
y in dom (carr X) holds
g . y in (carr X) . y ) )
by A5, CARD_3:def 5;
A32:
ex
g being
Function st
(
(reproj (k1,t2)) . ((a /. k1) * (t . k1)) = g &
dom g = dom (carr X) & ( for
y being
object st
y in dom (carr X) holds
g . y in (carr X) . y ) )
by A5, CARD_3:def 5;
reconsider RK =
(reproj (k1,t2)) . ((a /. k1) * (t . k1)) as
Function ;
for
x being
object st
x in dom t1 holds
t1 . x = RK . x
then A50:
t1 = (reproj (k1,t2)) . ((a /. k1) * (t . k1))
by A31, A32;
A53:
g . t1 =
(g * (reproj (k1,t2))) . ((a /. k1) * (t . k1))
by A50, FUNCT_2:15
.=
(a /. k1) * ((g * (reproj (k1,t2))) . (t . k1))
by A30, LOPBAN_1:def 5
.=
(a /. (k + 1)) * (g . ((reproj (k1,t2)) . (t . k1)))
by FUNCT_2:15
.=
(a /. (k + 1)) * (g . t2)
by A29, Th4X
;
thus g . t1 =
(a /. (k + 1)) * ((Product b2) * (g . t))
by A16, A17, A18, A25, A53, XXREAL_0:2
.=
((a /. (k + 1)) * (Product b2)) * (g . t)
by RLVECT_1:def 7
.=
(Product b) * (g . t)
by A23, RVSUM_1:96
;
verum
end;
A54:
for k being Nat holds S1[k]
from NAT_1:sch 2(A6, A15);
let t, t1 be Point of (product X); ( ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) implies g . t1 = (Product a) * (g . t) )
assume A55:
for i being Element of dom X holds t1 . i = (a /. i) * (t . i)
; g . t1 = (Product a) * (g . t)
set b = a | (len a);
A56:
( a | (len a) = a & len a <= len a )
by FINSEQ_2:20;
for i being Element of dom X holds
( ( i in Seg (len a) implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg (len a) implies t1 . i = t . i ) )
hence
g . t1 = (Product a) * (g . t)
by A54, A56; verum