let V be free finite-rank Z_Module; for F being linear-FrFunctional of V
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)))
let F be linear-FrFunctional of V; 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)))
defpred S1[ 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 S1[y] holds
S1[y ^ <*w*>]
proof
let y be
FinSequence of
V;
for w being Element of V st S1[y] holds
S1[y ^ <*w*>]let w be
Element of
V;
( S1[y] implies S1[y ^ <*w*>] )
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)))
;
S1[y ^ <*w*>]
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*>))))
verumproof
let x be
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*>))))let X,
Y be
FinSequence of
F_Real;
( 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) ) implies X "*" Y = F . (Sum (lmlt (x,(y ^ <*w*>)))) )
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)
;
X "*" Y = F . (Sum (lmlt (x,(y ^ <*w*>))))
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;
( k in Seg (len (x | (len y))) implies (Y | (len y)) . k = F . (y /. k) )
assume Q31:
k in Seg (len (x | (len y)))
;
(Y | (len y)) . k = F . (y /. k)
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
;
verum
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;
( k in dom (mlt (X,Y)) implies (mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k )
assume V1:
k in dom (mlt (X,Y))
;
(mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . k
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
( k <= len y or not k <= len y )
;
suppose
k <= len y
;
(mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . kthen 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
;
verum end; suppose
not
k <= len y
;
(mlt (X,Y)) . k = ((mlt ((X | (len y)),(Y | (len y)))) ^ <*((X /. ((len y) + 1)) * (Y /. ((len y) + 1)))*>) . kthen
(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
;
verum end; end;
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;
( k in dom (lmlt (x,(y ^ <*w*>))) implies (lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k )
assume V1:
k in dom (lmlt (x,(y ^ <*w*>)))
;
(lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . k
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
( k <= len y or not k <= len y )
;
suppose VX3:
k <= len y
;
(lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . kthen 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
;
verum end; suppose
not
k <= len y
;
(lmlt (x,(y ^ <*w*>))) . k = ((lmlt ((x | (len y)),y)) ^ <*((x /. ((len y) + 1)) * w)*>) . kthen
(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
;
verum end; end;
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
;
verum
end;
end;
A4:
S1[ <*> the carrier of V]
proof
let x be
FinSequence of
INT.Ring;
for X, Y being FinSequence of F_Real st X = x & len (<*> the carrier of V) = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . ((<*> the carrier of V) /. k) ) holds
X "*" Y = F . (Sum (lmlt (x,(<*> the carrier of V))))let X,
Y be
FinSequence of
F_Real;
( X = x & len (<*> the carrier of V) = len x & len X = len Y & ( for k being Nat st k in Seg (len x) holds
Y . k = F . ((<*> the carrier of V) /. k) ) implies X "*" Y = F . (Sum (lmlt (x,(<*> the carrier of V)))) )
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)
;
X "*" Y = F . (Sum (lmlt (x,(<*> the carrier of V))))
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
;
verum
end;
for p being FinSequence of V holds S1[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)))
; verum