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:119;
then dom (the multF of K .: x,(Base_FinSeq K,m,i)) = (dom x) /\ (dom (Base_FinSeq K,m,i)) by FUNCOP_1:84;
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:24;
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 10; :: thesis: |(x,(Base_FinSeq K,m,i))| = x /. i
x . i = x /. i by A1, A2, FINSEQ_4:24;
hence |(x,(Base_FinSeq K,m,i))| = x /. i by A8, FVSUM_1:def 10; :: thesis: verum
reconsider q = mlt x,(Base_FinSeq K,m,i) as FinSequence of K ;