let m, i be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( |(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; :: thesis: |(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; :: thesis: verum