let X be RealLinearSpace-Sequence; :: thesis: for Y being RealLinearSpace
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)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) holds
g . t1 = (Product a) * (g . t)
let Y be RealLinearSpace; :: 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)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . 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)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . 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)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) holds
g . t1 = (Product a) * (g . t) )
assume A1: dom a = dom X ; :: thesis: for t, t1 being Point of (product X)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) holds
g . t1 = (Product a) * (g . t)
A4: dom (carr X) = dom X by LemmaX;
defpred S₁[ Nat] means for t, t1 being Point of (product X)
for s, s1 being Element of product (carr X)
for b being FinSequence of REAL st t = s & t1 = s1 & b = a | $1 & $1 <= len a & ( for i being Element of dom X holds
( ( i in Seg $1 implies s1 . i = (a /. i) * (s . i) ) & ( not i in Seg $1 implies s1 . i = s . i ) ) ) holds
g . t1 = (Product b) * (g . t);
A6: S₁[ 0 ]

proof

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

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A17: S₁[k] ; :: thesis: S₁[k + 1]
let t, t1 be Point of (product X); :: thesis: for s, s1 being Element of product (carr X)
for b being FinSequence of REAL st t = s & t1 = s1 & b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies s1 . i = (a /. i) * (s . i) ) & ( not i in Seg (k + 1) implies s1 . i = s . i ) ) ) holds
g . t1 = (Product b) * (g . t)
let s, s1 be Element of product (carr X); :: thesis: for b being FinSequence of REAL st t = s & t1 = s1 & b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies s1 . i = (a /. i) * (s . i) ) & ( not i in Seg (k + 1) implies s1 . i = s . i ) ) ) holds
g . t1 = (Product b) * (g . t)
let b be FinSequence of REAL ; :: thesis: ( t = s & t1 = s1 & b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies s1 . i = (a /. i) * (s . i) ) & ( not i in Seg (k + 1) implies s1 . i = s . i ) ) ) implies g . t1 = (Product b) * (g . t) )
assume A18: ( t = s & t1 = s1 & b = a | (k + 1) & k + 1 <= len a & ( for i being Element of dom X holds
( ( i in Seg (k + 1) implies s1 . i = (a /. i) * (s . i) ) & ( not i in Seg (k + 1) implies s1 . i = s . i ) ) ) ) ; :: thesis: g . t1 = (Product b) * (g . t)
reconsider b2 = a | k as FinSequence of REAL ;
A19: k <= k + 1 by NAT_1:11;
( 1 <= k + 1 & k + 1 <= len a ) by A18, NAT_1:11;
then B20: k + 1 in Seg (len a) ;
then A21: k + 1 in dom a by FINSEQ_1:def 3;
A23: b2 = b | k by A18, FINSEQ_1:82, NAT_1:11;
A25: b = b2 ^ <*(b . (k + 1))*> by A18, A23, FINSEQ_1:59, FINSEQ_3:55
.= b2 ^ <*(a . (k + 1))*> by A18, FINSEQ_1:4, FUNCT_1:49
.= b2 ^ <*(a /. (k + 1))*> by A21, 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) * (s . $1);
deffunc H₂( Element of dom X) -> Element of the carrier of (X . $1) = s . $1;
consider s2 being Function such that
A26: ( 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) * (s . i) by A26;
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 = s . i by A26;
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, A26, CARD_3:def 5;
reconsider t2 = s2 as Point of (product X) ;
reconsider k1 = k + 1 as Element of dom X by A1, B20, FINSEQ_1:def 3;
k + 0 < k + 1 by XREAL_1:8;
then not k1 in Seg k by FINSEQ_1:1;
then A30: s2 . k1 = s . k1 by A26;
A31: g * (reproj (k1,t2)) is LinearOperator of (X . k1),Y by Def3;
set RK = (reproj (k1,t2)) . ((a /. k1) * (s . k1));
A32: ex g being Function st
( s1 = g & dom g = dom (carr X) & ( for y being object st y in dom (carr X) holds
g . y in (carr X) . y ) ) by CARD_3:def 5;
A33: ex g being Function st
( (reproj (k1,t2)) . ((a /. k1) * (s . 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 CARD_3:def 5;
reconsider RK = (reproj (k1,t2)) . ((a /. k1) * (s . k1)) as Function ;
A51: for x being object st x in dom s1 holds
s1 . x = RK . x

proof

let x be object ; :: thesis: ( x in dom s1 implies s1 . x = RK . x )
assume x in dom s1 ; :: thesis: s1 . x = RK . x
then reconsider i = x as Element of dom X by LemmaX, A32;
A38: ( ( i in Seg k implies s2 . i = (a /. i) * (s . i) ) & ( not i in Seg k implies s2 . i = s . i ) ) by A26;
A40: ( i <> k1 implies RK . i = s2 . i ) by Th4;

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

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

then A42: s1 . i = (a /. i) * (s . i) by A18;

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

suppose A43: i = k + 1 ; :: thesis: s1 . x = RK . x

then RK . i = (a /. k1) * (s . k1) by Th3
.= s1 . i by A18, A41, A43 ;
hence s1 . x = RK . x ; :: thesis: verum

end;

suppose A44: i <> k + 1 ; :: thesis: s1 . x = RK . x

( 1 <= i & i <= k + 1 ) by A41, FINSEQ_1:1;
then ( 1 <= i & i < k + 1 ) by A44, XXREAL_0:1;
then ( 1 <= i & i <= k ) by NAT_1:13;
hence s1 . x = RK . x by A38, A42, A44, Th4; :: thesis: verum

end;

end;

end;

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

i in dom X ;
then i in Seg (len X) by FINSEQ_1:def 3;
then A47: ( 1 <= i & i <= len X ) by FINSEQ_1:1;
A49: k + 1 < i by A46, A47;
k <= k + 1 by NAT_1:11;
then k < i by A49, XXREAL_0:2;
hence s1 . x = RK . x by A18, A38, A40, A46, A47, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

A54: g . t1 = g . ((reproj (k1,t2)) . ((a /. k1) * (s . k1))) by A18, A32, A33, A51, FUNCT_1:2
.= (g * (reproj (k1,t2))) . ((a /. k1) * (s . k1)) by FUNCT_2:15
.= (a /. k1) * ((g * (reproj (k1,t2))) . (s . k1)) by A31, LOPBAN_1:def 5
.= (a /. (k + 1)) * (g . ((reproj (k1,t2)) . (s . k1))) by FUNCT_2:15
.= (a /. (k + 1)) * (g . t2) by A30, Th4X ;
thus g . t1 = (a /. (k + 1)) * ((Product b2) * (g . t)) by A17, A18, A19, A26, A54, XXREAL_0:2
.= ((a /. (k + 1)) * (Product b2)) * (g . t) by RLVECT_1:def 7
.= (Product b) * (g . t) by A25, RVSUM_1:96 ; :: thesis: verum

end;

A55: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A16);
let t, t1 be Point of (product X); :: thesis: for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) holds
g . t1 = (Product a) * (g . t)
let s, s1 be Element of product (carr X); :: thesis: ( t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) implies g . t1 = (Product a) * (g . t) )
assume A56: ( t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) ) ; :: thesis: g . t1 = (Product a) * (g . t)
set b = a | (len a);
A57: ( 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 s1 . i = (a /. i) * (s . i) ) & ( not i in Seg (len a) implies s1 . i = s . i ) )

proof

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

proof

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

end;

end;

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