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:27;
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:24;
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: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 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:3;
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 16
.= x . i by A5, PARTFUN1:def 8 ;
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:24
.= 0. K by A10, A11, A12, Th25 ;
j in dom (mlt x,(Base_FinSeq K,m,i)) by A9, A11, A12, FINSEQ_1:3;
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:36 ;
hence y . j = 0. K by A2; :: thesis: verum