let i, n be Nat; for x being Element of REAL n st 1 <= i & i <= n holds
|(x,(Base_FinSeq (n,i)))| = x . i
let x be Element of REAL n; ( 1 <= i & i <= n implies |(x,(Base_FinSeq (n,i)))| = x . i )
assume that
A1:
1 <= i
and
A2:
i <= n
; |(x,(Base_FinSeq (n,i)))| = x . i
set x2 = Base_FinSeq (n,i);
A3:
len x = n
by CARD_1:def 7;
A4:
len (Base_FinSeq (n,i)) = n
by MATRIXR2:74;
then A5:
len (mlt (x,(Base_FinSeq (n,i)))) = n
by A3, MATRPROB:30;
A6:
for j being Nat st 1 <= j & j <= n holds
(mlt (x,(Base_FinSeq (n,i)))) . j = ((x /. i) * (Base_FinSeq (n,i))) . j
proof
let j be
Nat;
( 1 <= j & j <= n implies (mlt (x,(Base_FinSeq (n,i)))) . j = ((x /. i) * (Base_FinSeq (n,i))) . j )
assume that A7:
1
<= j
and A8:
j <= n
;
(mlt (x,(Base_FinSeq (n,i)))) . j = ((x /. i) * (Base_FinSeq (n,i))) . j
reconsider j0 =
j as
Element of
NAT by ORDINAL1:def 12;
(mlt (x,(Base_FinSeq (n,i)))) . j = (x . j) * ((Base_FinSeq (n,i)) . j)
by RVSUM_1:59;
hence
(mlt (x,(Base_FinSeq (n,i)))) . j = ((x /. i) * (Base_FinSeq (n,i))) . j
by A3, A7, A8, A9, FINSEQ_4:15;
verum
end;
len ((x /. i) * (Base_FinSeq (n,i))) = n
by A4, RVSUM_1:117;
then
mlt (x,(Base_FinSeq (n,i))) = (x /. i) * (Base_FinSeq (n,i))
by A5, A6, FINSEQ_1:14;
then Sum (mlt (x,(Base_FinSeq (n,i)))) =
(x /. i) * (Sum (Base_FinSeq (n,i)))
by RVSUM_1:87
.=
(x /. i) * 1
by A1, A2, Th26
.=
x . i
by A1, A2, A3, FINSEQ_4:15
;
hence
|(x,(Base_FinSeq (n,i)))| = x . i
; verum