let K be Field; :: thesis: for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt p,q) = q . i
let p, q be FinSequence of K; :: thesis: for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt p,q) = q . i
let i be Nat; :: thesis: ( i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies Sum (mlt p,q) = q . i )
assume that
A1: ( i in dom p & i in dom q & p . i = 1. K ) and
A2: for k being Nat st k in dom p & k <> i holds
p . k = 0. K ; :: thesis: Sum (mlt p,q) = q . i
reconsider r = mlt p,q as FinSequence of K ;
A3: ( i in dom r & r . i = q . i )

proof

A4: ( dom p = Seg (len p) & dom q = Seg (len q) & dom (mlt p,q) = Seg (len (mlt p,q)) ) by FINSEQ_1:def 3;
len (mlt p,q) = min (len p),(len q) by Th15;
then A5: (dom p) /\ (dom q) = dom (mlt p,q) by A4, FINSEQ_2:2;
then A6: i in dom (mlt p,q) by A1, XBOOLE_0:def 4;
thus i in dom r by A1, A5, XBOOLE_0:def 4; :: thesis: r . i = q . i
thus r . i = q . i by A1, A2, A6, Th16; :: thesis: verum

end;

for k being Nat st k in dom r & k <> i holds
r . k = 0. K by A1, A2, Th16;
hence Sum (mlt p,q) = q . i by A3, Th14; :: thesis: verum
thus verum ; :: thesis: verum