let V be free finite-rank Z_Module; :: thesis:
let F be linear-FrFunctional of V; :: thesis:
defpred S₁[ FinSequence of V] means for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real st X = x & len $1 = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . ($1 /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,$1)));
A2: for y being FinSequence of V
for w being Element of V st S₁[y] holds
S₁[y ^ <*w*>]

proof

let y be FinSequence of V; :: thesis:
let w be Element of V; :: thesis:
assume P1: for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . (y /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,y))) ; :: thesis:
thus for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real st X = x & len (y ^ <*w*>) = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . ((y ^ <*w*>) /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,(y ^ <*w*>)))) :: thesis:

proof

let x be FinSequence of INT.Ring; :: thesis:
let X, Y be FinSequence of F_Real; :: thesis:
assume that
R1: X = x and
R2: len (y ^ <*w*>) = len x and
R3: len X = len Y and
R4: for k being Nat st k in Seg (len x) holds
Y . k = F . ((y ^ <*w*>) /. k) ; :: thesis:
X1: F is additive ;
X2: F is homogeneous ;
set n = len y;
set X0 = X | (len y);
set Y0 = Y | (len y);
set x0 = x | (len y);
Q0: len (y ^ <*w*>) = (len y) + (len <*w*>) by FINSEQ_1:22
.= (len y) + 1 by FINSEQ_1:39 ;
LN4: len (x | (len y)) = len y by Q0, R2, FINSEQ_1:59, NAT_1:11;
LN5: len (X | (len y)) = len y by Q0, R1, R2, FINSEQ_1:59, NAT_1:11;
LN6: len (Y | (len y)) = len y by Q0, R1, R2, R3, FINSEQ_1:59, NAT_1:11;
LN7: (len y) + 1 in Seg ((len y) + 1) by FINSEQ_1:4;
Q2: len y = len (x | (len y)) by Q0, R2, FINSEQ_1:59, NAT_1:11;
Q3: len (X | (len y)) = len (Y | (len y)) by LN5, Q0, R1, R2, R3, FINSEQ_1:59, NAT_1:11;
for k being Nat st k in Seg (len (x | (len y))) holds
(Y | (len y)) . k = F . (y /. k)

proof

let k be Nat; :: thesis:
assume Q31: k in Seg (len (x | (len y))) ; :: thesis:
then Q34: k in dom y by LN4, FINSEQ_1:def 3;
Q32: Seg (len (x | (len y))) c= Seg (len x) by FINSEQ_3:18, Q0, R2, LN4;
then k in Seg (len x) by Q31;
then Q33: k in dom (y ^ <*w*>) by R2, FINSEQ_1:def 3;
Q35: (y ^ <*w*>) /. k = (y ^ <*w*>) . k by Q33, PARTFUN1:def 6
.= y . k by FINSEQ_1:def 7, Q34
.= y /. k by Q34, PARTFUN1:def 6 ;
thus (Y | (len y)) . k = Y . k by LN4, Q31, FUNCT_1:49
.= F . (y /. k) by R4, Q31, Q32, Q35 ; :: thesis:

end;

then Q4: (X | (len y)) "*" (Y | (len y)) = F . (Sum (lmlt ((x | (len y)),y))) by R1, Q2, Q3, P1;
Q51: (len y) + 1 in dom X by LN7, Q0, R1, R2, FINSEQ_1:def 3;
Q61: (len y) + 1 in dom Y by LN7, Q0, R1, R2, R3, FINSEQ_1:def 3;
Q71: (len y) + 1 in dom x by LN7, Q0, R2, FINSEQ_1:def 3;
Q9: X /. ((len y) + 1) = X . ((len y) + 1) by Q51, PARTFUN1:def 6
.= x /. ((len y) + 1) by R1, Q71, PARTFUN1:def 6 ;
Q103: (len y) + 1 in dom (y ^ <*w*>) by LN7, Q0, FINSEQ_1:def 3;
Q102: (y ^ <*w*>) /. ((len y) + 1) = (y ^ <*w*>) . ((len y) + 1) by Q103, PARTFUN1:def 6
.= w by FINSEQ_1:42 ;
Y /. ((len y) + 1) = Y . ((len y) + 1) by Q61, PARTFUN1:def 6
.= F . w by Q0, Q102, R2, R4, FINSEQ_1:4 ;
then Q11: (X /. ((len y) + 1)) * (Y /. ((len y) + 1)) = F . ((x /. ((len y) + 1)) * w) by Q9, X2;
len (mlt (X,Y)) = (len y) + 1 by Q0, R1, R2, R3, MATRIX_3:6;
then Q85: dom (mlt (X,Y)) = Seg ((len y) + 1) by FINSEQ_1:def 3;
Q82: len (mlt ((X | (len y)),(Y | (len y)))) = len y by LN5, LN6, MATRIX_3:6;
len ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) = (len (mlt ((X | (len y)),(Y | (len y))))) + (len <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) by FINSEQ_1:22
.= (len y) + 1 by Q82, FINSEQ_1:39 ;
then DM1: dom (mlt (X,Y)) = dom ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) by Q85, FINSEQ_1:def 3;
for k being Nat st k in dom (mlt (X,Y)) holds
(mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k

proof

let k be Nat; :: thesis:
assume V1: k in dom (mlt (X,Y)) ; :: thesis:
then V2: ( 1 <= k & k <= (len y) + 1 ) by Q85, FINSEQ_1:1;
set f = (mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>;

per cases ;

suppose k <= len y ; :: thesis:

then V3: k in Seg (len y) by V2;
then V4: k in dom (mlt ((X | (len y)),(Y | (len y)))) by Q82, FINSEQ_1:def 3;
V5: k in dom (X | (len y)) by LN5, V3, FINSEQ_1:def 3;
V6: k in dom (Y | (len y)) by LN6, V3, FINSEQ_1:def 3;
(X | (len y)) . k in rng (X | (len y)) by V5, FUNCT_1:3;
then reconsider X0k = (X | (len y)) . k as Element of F_Real ;
(Y | (len y)) . k in rng (Y | (len y)) by V6, FUNCT_1:3;
then reconsider Y0k = (Y | (len y)) . k as Element of F_Real ;
k in dom X by V1, Q0, Q85, R1, R2, FINSEQ_1:def 3;
then X . k in rng X by FUNCT_1:3;
then reconsider Xk = X . k as Element of F_Real ;
k in dom Y by V1, Q0, Q85, R1, R2, R3, FINSEQ_1:def 3;
then Y . k in rng Y by FUNCT_1:3;
then reconsider Yk = Y . k as Element of F_Real ;
((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k = (mlt ((X | (len y)),(Y | (len y)))) . k by V4, FINSEQ_1:def 7
.= X0k * Y0k by V4, FVSUM_1:60
.= (X . k) * ((Y | (len y)) . k) by V5, FUNCT_1:47
.= Xk * Yk by V6, FUNCT_1:47
.= (mlt (X,Y)) . k by V1, FVSUM_1:60 ;
hence (mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k ; :: thesis:

end;

suppose not k <= len y ; :: thesis:

then (len y) + 1 <= k by NAT_1:13;
then V8: k = (len y) + 1 by XXREAL_0:1, V2;
Seg 1 = dom <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*> by FINSEQ_1:38;
then V10: 1 in dom <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*> ;
Q9: X /. ((len y) + 1) = X . ((len y) + 1) by Q51, PARTFUN1:def 6;
then reconsider Xn = X . ((len y) + 1) as Element of F_Real ;
Q10: Y /. ((len y) + 1) = Y . ((len y) + 1) by Q61, PARTFUN1:def 6;
then reconsider Yn = Y . ((len y) + 1) as Element of F_Real ;
((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k = <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*> . 1 by Q82, FINSEQ_1:def 7, V8, V10
.= (X /. ((len y) + 1)) * (Y /. ((len y) + 1)) by FINSEQ_1:40
.= (mlt (X,Y)) . k by Q9, Q10, V1, V8, FVSUM_1:60 ;
hence (mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k ; :: thesis:

end;

then Q8: mlt (X,Y) = (mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*> by DM1, FINSEQ_1:13;
QX121: dom x = Seg ((len y) + 1) by Q0, R2, FINSEQ_1:def 3
.= dom (y ^ <*w*>) by Q0, FINSEQ_1:def 3 ;
then Q121: dom (lmlt (x,(y ^ <*w*>))) = dom x by ZMATRLIN:13;
dom (x | (len y)) = Seg (len y) by FINSEQ_1:def 3, LN4
.= dom y by FINSEQ_1:def 3 ;
then dom (lmlt ((x | (len y)),y)) = dom (x | (len y)) by ZMATRLIN:13;
then Q124: dom (lmlt ((x | (len y)),y)) = Seg (len y) by LN4, FINSEQ_1:def 3;
then Q125: len (lmlt ((x | (len y)),y)) = len y by FINSEQ_1:def 3;
len ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) = (len (lmlt ((x | (len y)),y))) + (len <*((x /. ((len y) + 1)) * w)*>) by FINSEQ_1:22
.= (len y) + 1 by Q125, FINSEQ_1:39 ;
then dom ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) = Seg ((len y) + 1) by FINSEQ_1:def 3;
then DM1: dom (lmlt (x,(y ^ <*w*>))) = dom ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) by Q0, Q121, R2, FINSEQ_1:def 3;
for k being Nat st k in dom (lmlt (x,(y ^ <*w*>))) holds
(lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k

proof

let k be Nat; :: thesis:
assume V1: k in dom (lmlt (x,(y ^ <*w*>))) ; :: thesis:
then V0: k in Seg ((len y) + 1) by Q121, Q0, R2, FINSEQ_1:def 3;
then V2: ( 1 <= k & k <= (len y) + 1 ) by FINSEQ_1:1;
set f = (lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>;

per cases ;

suppose VX3: k <= len y ; :: thesis:

then V3: k in Seg (len y) by V2;
V5: k in dom (x | (len y)) by V3, LN4, FINSEQ_1:def 3;
V6: k in dom y by V3, FINSEQ_1:def 3;
rng (x | (len y)) c= the carrier of INT.Ring ;
then reconsider x0k = (x | (len y)) . k as Element of INT.Ring by V5, FUNCT_1:3;
y . k in rng y by V6, FUNCT_1:3;
then reconsider y0k = y . k as Element of V ;
XX2: k in dom x by V1, QX121, ZMATRLIN:13;
rng x c= the carrier of INT.Ring ;
then reconsider xk = x . k as Element of INT.Ring by XX2, FUNCT_1:3;
k in dom (y ^ <*w*>) by V0, Q0, FINSEQ_1:def 3;
then (y ^ <*w*>) . k in rng (y ^ <*w*>) by FUNCT_1:3;
then reconsider yk = (y ^ <*w*>) . k as Element of V ;
W: y0k = yk by V6, FINSEQ_1:def 7;
((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k = (lmlt ((x | (len y)),y)) . k by V3, Q124, FINSEQ_1:def 7
.= x0k * y0k by V2, VX3, Q124, FUNCOP_1:22, FINSEQ_1:1
.= xk * y0k by V5, FUNCT_1:47
.= (lmlt (x,(y ^ <*w*>))) . k by W, V1, FUNCOP_1:22 ;
hence (lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k ; :: thesis:

end;

suppose not k <= len y ; :: thesis:

then (len y) + 1 <= k by NAT_1:13;
then V8: k = (len y) + 1 by XXREAL_0:1, V2;
Seg 1 = dom <*((x /. ((len y) + 1)) * w)*> by FINSEQ_1:38;
then V10: 1 in dom <*((x /. ((len y) + 1)) * w)*> ;
Seg 1 = dom <*w*> by FINSEQ_1:38;
then V11: 1 in dom <*w*> ;
Q9: x /. ((len y) + 1) = x . ((len y) + 1) by Q71, PARTFUN1:def 6;
then reconsider xn = x . ((len y) + 1) as Element of INT.Ring ;
(y ^ <*w*>) /. ((len y) + 1) = (y ^ <*w*>) . ((len y) + 1) by Q103, PARTFUN1:def 6;
then reconsider yn = (y ^ <*w*>) . ((len y) + 1) as Element of V ;
Q11: (y ^ <*w*>) . ((len y) + 1) = <*w*> . 1 by V11, FINSEQ_1:def 7
.= w by FINSEQ_1:40 ;
((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k = <*((x /. ((len y) + 1)) * w)*> . 1 by Q125, V8, V10, FINSEQ_1:def 7
.= xn * w by Q9, FINSEQ_1:40
.= (lmlt (x,(y ^ <*w*>))) . k by Q11, V1, V8, FUNCOP_1:22 ;
hence (lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k ; :: thesis:

end;

then Q12: lmlt (x,(y ^ <*w*>)) = (lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*> by DM1, FINSEQ_1:13;
thus X "*" Y = (Sum (mlt ((X | (len y)),(Y | (len y))))) + ((X /. ((len y) + 1)) * (Y /. ((len y) + 1))) by FVSUM_1:71, Q8
.= F . ((Sum (lmlt ((x | (len y)),y))) + ((x /. ((len y) + 1)) * w)) by Q4, Q11, X1
.= F . (Sum (lmlt (x,(y ^ <*w*>)))) by FVSUM_1:71, Q12 ; :: thesis:

end;

A4: S₁[ <*> the carrier of V]

proof

let x be FinSequence of INT.Ring; :: thesis:
let X, Y be FinSequence of F_Real; :: thesis:
assume that
R1: X = x and
R2: len (<*> the carrier of V) = len x and
len X = len Y and
for k being Nat st k in Seg (len x) holds
Y . k = F . ((<*> the carrier of V) /. k) ; :: thesis:
set y = <*> the carrier of V;
Q2: X = <*> the carrier of F_Real by R1, R2;
Q4: mlt (X,Y) = <*> the carrier of F_Real by Q2;
reconsider I0 = 0 as Element of INT.Ring ;
X1: F is additive ;
X2: F . (0. V) = F . ((0. V) + (0. V))
.= (F . (0. V)) + (F . (0. V)) by X1 ;
thus X "*" Y = 0. F_Real by Q4, RLVECT_1:43
.= F . (Sum (lmlt (x,(<*> the carrier of V)))) by X2, RLVECT_1:43 ; :: thesis:

end;

for p being FinSequence of V holds S₁[p] from FINSEQ_2:sch 2(A4, A2);
hence for y being FinSequence of V
for x being FinSequence of INT.Ring
for X, Y being FinSequence of F_Real st X = x & len y = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . (y /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,y))) ; :: thesis: