let K be Field; :: thesis: for p, q being FinSequence of K
for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let p, q be FinSequence of K; :: thesis: for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let i be Nat; :: thesis: ( p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) ) )
assume that
A1: p . i = 1. K and
A2: for k being Nat st k in dom p & k <> i holds
p . k = 0. K ; :: thesis: for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
let j be Nat; :: thesis: ( j in dom (mlt (p,q)) implies ( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) ) )
assume A3: j in dom (mlt (p,q)) ; :: thesis: ( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )
A4: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
reconsider j1 = j as Element of NAT by ORDINAL1:def 12;
( dom (mlt (p,q)) = Seg (len (mlt (p,q))) & len (mlt (p,q)) = min ((len p),(len q)) ) by Th15, FINSEQ_1:def 3;
then A5: j in (dom p) /\ (dom q) by A3, A4, FINSEQ_2:2;
then A6: j in dom q by XBOOLE_0:def 4;
then reconsider b = q . j1 as Element of K by FINSEQ_2:11;
thus ( i = j implies (mlt (p,q)) . j = q . i ) :: thesis: ( i <> j implies (mlt (p,q)) . j = 0. K )

proof

reconsider b = q . j1 as Element of K by A6, FINSEQ_2:11;
assume A7: i = j ; :: thesis: (mlt (p,q)) . j = q . i
hence (mlt (p,q)) . j = b * (1. K) by A1, A3, FVSUM_1:60
.= q . i by A7, VECTSP_1:def 8 ;
:: thesis: verum

end;

assume A8: i <> j ; :: thesis: (mlt (p,q)) . j = 0. K
j in dom p by A5, XBOOLE_0:def 4;
then p . j = 0. K by A2, A8;
hence (mlt (p,q)) . j = (0. K) * b by A3, FVSUM_1:60
.= 0. K by VECTSP_1:12 ;
:: thesis: verum