let X be RealNormSpace-Sequence; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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: S₁[ 0 ]

proof

let t, t1 be Point of (product X); :: thesis: for b being FinSequence of REAL st b = a | 0 & 0 <= len a & ( for i being Element of dom X holds
( ( i in Seg 0 implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg 0 implies t1 . i = t . i ) ) ) holds
g . t1 = (Product b) * (g . t)
let b be FinSequence of REAL ; :: thesis: ( b = a | 0 & 0 <= len a & ( for i being Element of dom X holds
( ( i in Seg 0 implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg 0 implies t1 . i = t . i ) ) ) implies g . t1 = (Product b) * (g . t) )
assume A7: ( b = a | 0 & 0 <= len a & ( for i being Element of dom X holds
( ( i in Seg 0 implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg 0 implies t1 . i = t . i ) ) ) ) ; :: thesis: g . t1 = (Product b) * (g . t)
A10: 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;
A11: ex g being Function st
( t = 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;
t1 = t by A4, A7, A10, A11;
hence g . t1 = (Product b) * (g . t) by A7, RLVECT_1:def 8, RVSUM_1:94; :: thesis: verum

end;

A15: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A16: S₁[k] ; :: thesis: S₁[k + 1]
let t, t1 be Point of (product X); :: thesis: 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 ; :: thesis: ( 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 ) ) ) ) ; :: thesis: 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 S₂[ object ] means $1 in Seg k;
deffunc H₁( Element of dom X) -> Element of the carrier of (X . $1) = (a /. $1) * (t . $1);
deffunc H₂( 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
( ( S₂[i] implies s2 . i = H₁(i) ) & ( not S₂[i] implies s2 . i = H₂(i) ) ) ) ) from PARTFUN1:sch 4();
for y being object st y in dom (carr X) holds
s2 . y in (carr X) . y

proof

let y be object ; :: thesis: ( y in dom (carr X) implies s2 . y in (carr X) . y )
assume y in dom (carr X) ; :: thesis: s2 . y in (carr X) . y
then reconsider i = y as Element of dom X by LemmaX;

per cases ( S₂[i] or not S₂[i] ) ;

suppose S₂[i] ; :: thesis: s2 . y in (carr X) . y

then s2 . y = (a /. i) * (t . i) by A25;
then s2 . y in the carrier of (X . i) ;
hence s2 . y in (carr X) . y by PRVECT_1:def 11; :: thesis: verum

end;

suppose not S₂[i] ; :: thesis: s2 . y in (carr X) . y

then s2 . y = t . i by A25;
then s2 . y in the carrier of (X . i) ;
hence s2 . y in (carr X) . y by PRVECT_1:def 11; :: thesis: verum

end;

end;

end;

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

proof

let x be object ; :: thesis: ( x in dom t1 implies t1 . x = RK . x )
assume x in dom t1 ; :: thesis: t1 . x = RK . x
then reconsider i = x as Element of dom X by LemmaX, A31;
A37: ( ( i in Seg k implies s2 . i = (a /. i) * (t . i) ) & ( not i in Seg k implies s2 . i = t . i ) ) by A25;

per cases ( i in Seg (k + 1) or not i in Seg (k + 1) ) ;

suppose A40: i in Seg (k + 1) ; :: thesis: t1 . x = RK . x

per cases ( i = k + 1 or i <> k + 1 ) ;

suppose A42: i = k + 1 ; :: thesis: t1 . x = RK . x

then RK . i = (a /. k1) * (t . k1) by Th3
.= t1 . i by A17, A40, A42 ;
hence t1 . x = RK . x ; :: thesis: verum

end;

suppose A43: i <> k + 1 ; :: thesis: t1 . x = RK . x

then A44: RK . i = s2 . i by Th4;
( 1 <= i & i <= k + 1 ) by A40, FINSEQ_1:1;
then ( 1 <= i & i < k + 1 ) by A43, XXREAL_0:1;
then ( 1 <= i & i <= k ) by NAT_1:13;
hence t1 . x = RK . x by A17, A37, A40, A44; :: thesis: verum

end;

end;

end;

suppose A45: not i in Seg (k + 1) ; :: thesis: t1 . x = RK . x

A46: ( 1 <= i & i <= len X ) by FINSEQ_3:25;
A48: k + 1 < i by A45, A46;
then A49: RK . i = s2 . i by Th4;
k <= k + 1 by NAT_1:11;
then k < i by A48, XXREAL_0:2;
hence t1 . x = RK . x by A17, A37, A45, A49, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

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 ; :: thesis: verum

end;

A54: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A15);
let t, t1 be Point of (product X); :: thesis: ( ( 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) ; :: thesis: 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 ) )

proof

let i be Element of dom X; :: thesis: ( ( i in Seg (len a) implies t1 . i = (a /. i) * (t . i) ) & ( not i in Seg (len a) implies t1 . i = t . i ) )
thus ( i in Seg (len a) implies t1 . i = (a /. i) * (t . i) ) by A55; :: thesis: ( not i in Seg (len a) implies t1 . i = t . i )
thus ( not i in Seg (len a) implies t1 . i = t . i ) :: thesis: verum

proof

assume not i in Seg (len a) ; :: thesis: t1 . i = t . i
then not i in dom X by A1, FINSEQ_1:def 3;
hence t1 . i = t . i ; :: thesis: verum

end;

end;

hence g . t1 = (Product a) * (g . t) by A54, A56; :: thesis: verum