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 A1: ( len x = m & y = mlt x,(Base_FinSeq K,m,i) & 1 <= i & 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 ) )
A2: i in dom x by A1, FINSEQ_3:27;
A3: len (Base_FinSeq K,m,i) = m by AA1100;
A4: dom the multF of K = [:the carrier of K,the carrier of K:] by FUNCT_2:def 1;
A5: rng x c= the carrier of K by FINSEQ_1:def 4;
B1: rng (Base_FinSeq K,m,i) c= the carrier of K by FINSEQ_1:def 4;
B2: [:(rng x),(rng (Base_FinSeq K,m,i)):] c= dom the multF of K by A5, A4, B1, ZFMISC_1:119;
B3: dom (the multF of K .: x,(Base_FinSeq K,m,i)) = (dom x) /\ (dom (Base_FinSeq K,m,i)) by B2, FUNCOP_1:84;
A5: dom (mlt x,(Base_FinSeq K,m,i)) = (dom x) /\ (dom (Base_FinSeq K,m,i)) by B3, FVSUM_1:def 7
.= (Seg m) /\ (dom (Base_FinSeq K,m,i)) by A1, FINSEQ_1:def 3
.= (Seg m) /\ (Seg m) by A3, FINSEQ_1:def 3
.= Seg m ;
then A4: i in dom (mlt x,(Base_FinSeq K,m,i)) by A1, FINSEQ_1:3;
C1: ( 1 <= i & i <= len (Base_FinSeq K,m,i) ) by A1, AA1100;
A32: (Base_FinSeq K,m,i) /. i = (Base_FinSeq K,m,i) . i by C1, FINSEQ_4:24;
(mlt x,(Base_FinSeq K,m,i)) . i = (x /. i) * ((Base_FinSeq K,m,i) /. i) by A4, FV73
.= (x /. i) * (1. K) by AA1110, A1, A32
.= x /. i by VECTSP_1:def 16
.= x . i by A2, PARTFUN1:def 8 ;
hence y . i = x . i by A1; :: 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 B1: ( j <> i & 1 <= j & j <= m ) ; :: thesis: y . j = 0. K
C2: ( 1 <= j & j <= len (Base_FinSeq K,m,i) ) by B1, AA1100;
C3: (Base_FinSeq K,m,i) /. j = (Base_FinSeq K,m,i) . j by C2, FINSEQ_4:24
.= 0. K by B1, AA1120, A1 ;
A4b: j in dom (mlt x,(Base_FinSeq K,m,i)) by A5, B1, FINSEQ_1:3;
(mlt x,(Base_FinSeq K,m,i)) . j = (x /. j) * ((Base_FinSeq K,m,i) /. j) by A4b, FV73
.= 0. K by C3, VECTSP_1:36 ;
hence y . j = 0. K by A1; :: thesis: verum