let m, i be Element of NAT ; for K being Field
for x being FinSequence of K st len x = m & 1 <= i & i <= m holds
( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )
let K be Field; for x being FinSequence of K st len x = m & 1 <= i & i <= m holds
( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )
let x be FinSequence of K; ( len x = m & 1 <= i & i <= m implies ( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i ) )
assume that
A1:
len x = m
and
A2:
( 1 <= i & i <= m )
; ( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )
A3:
for j being Element of NAT st j <> i & 1 <= j & j <= m holds
(mlt (x,(Base_FinSeq (K,m,i)))) . j = 0. K
by A1, A2, Th34;
A4:
len (Base_FinSeq (K,m,i)) = m
by Th23;
A5:
rng (Base_FinSeq (K,m,i)) c= the carrier of K
by FINSEQ_1:def 4;
( dom the multF of K = [: the carrier of K, the carrier of K:] & rng x c= the carrier of K )
by FINSEQ_1:def 4, FUNCT_2:def 1;
then
[:(rng x),(rng (Base_FinSeq (K,m,i))):] c= dom the multF of K
by A5, ZFMISC_1:96;
then
dom ( the multF of K .: (x,(Base_FinSeq (K,m,i)))) = (dom x) /\ (dom (Base_FinSeq (K,m,i)))
by FUNCOP_1:69;
then dom (mlt (x,(Base_FinSeq (K,m,i)))) =
(dom x) /\ (dom (Base_FinSeq (K,m,i)))
by FVSUM_1:def 7
.=
(Seg m) /\ (dom (Base_FinSeq (K,m,i)))
by A1, FINSEQ_1:def 3
.=
(Seg m) /\ (Seg m)
by A4, FINSEQ_1:def 3
.=
Seg m
;
then A6:
len (mlt (x,(Base_FinSeq (K,m,i)))) = m
by FINSEQ_1:def 3;
A7:
x /. i = x . i
by A1, A2, FINSEQ_4:15;
then
(mlt (x,(Base_FinSeq (K,m,i)))) . i = x /. i
by A1, A2, Th34;
then A8:
Sum (mlt (x,(Base_FinSeq (K,m,i)))) = x . i
by A2, A7, A6, A3, Th32;
hence
|(x,(Base_FinSeq (K,m,i)))| = x . i
by FVSUM_1:def 9; |(x,(Base_FinSeq (K,m,i)))| = x /. i
x . i = x /. i
by A1, A2, FINSEQ_4:15;
hence
|(x,(Base_FinSeq (K,m,i)))| = x /. i
by A8, FVSUM_1:def 9; verum