let m be Element of NAT ; :: thesis: for K being Field
for x, y being FinSequence of K
for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds
( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) )
let K be Field; :: thesis: for x, y being FinSequence of K
for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds
( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) )
let x, y be FinSequence of K; :: thesis: for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds
( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) )
let i be Element of NAT ; :: thesis: ( len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m implies ( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) ) )
assume that
A1: len x = m and
A2: y = mlt (x,(Base_FinSeq (K,m,i))) and
A3: 1 <= i and
A4: i <= m ; :: thesis: ( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) )
A5: i in dom x by A1, A3, A4, FINSEQ_3:25;
i <= len (Base_FinSeq (K,m,i)) by A4, Th23;
then A6: (Base_FinSeq (K,m,i)) /. i = (Base_FinSeq (K,m,i)) . i by A3, FINSEQ_4:15;
A7: rng (Base_FinSeq (K,m,i)) c= the carrier of K by FINSEQ_1:def 4;
A8: len (Base_FinSeq (K,m,i)) = m by Th23;
( 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 A7, 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 A9: 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 A8, FINSEQ_1:def 3
.= Seg m ;
then i in dom (mlt (x,(Base_FinSeq (K,m,i)))) by A3, A4, FINSEQ_1:1;
then (mlt (x,(Base_FinSeq (K,m,i)))) . i = (x /. i) * ((Base_FinSeq (K,m,i)) /. i) by Th4
.= (x /. i) * (1. K) by A3, A4, A6, Th24
.= x /. i by VECTSP_1:def 6
.= x . i by A5, PARTFUN1:def 6 ;
hence y . i = x . i by A2; :: thesis: for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K
let j be Element of NAT ; :: thesis: ( j <> i & 1 <= j & j <= m implies y . j = 0. K )
assume that
A10: j <> i and
A11: 1 <= j and
A12: j <= m ; :: thesis: y . j = 0. K
j <= len (Base_FinSeq (K,m,i)) by A12, Th23;
then A13: (Base_FinSeq (K,m,i)) /. j = (Base_FinSeq (K,m,i)) . j by A11, FINSEQ_4:15
.= 0. K by A10, A11, A12, Th25 ;
j in dom (mlt (x,(Base_FinSeq (K,m,i)))) by A9, A11, A12, FINSEQ_1:1;
then (mlt (x,(Base_FinSeq (K,m,i)))) . j = (x /. j) * ((Base_FinSeq (K,m,i)) /. j) by Th4
.= 0. K by A13, VECTSP_1:6 ;
hence y . j = 0. K by A2; :: thesis: verum