let K be Ring; :: 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 ) and
A2: ( p . i = 1. K & ( 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: for k being Nat st k in dom r & k <> i holds
r . k = 0. K by A2, Th14;
A4: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
( dom (mlt (p,q)) = Seg (len (mlt (p,q))) & len (mlt (p,q)) = min ((len p),(len q)) ) by Th13, FINSEQ_1:def 3;
then (dom p) /\ (dom q) = dom (mlt (p,q)) by A4, FINSEQ_2:2;
then A5: i in dom r by A1, XBOOLE_0:def 4;
then r . i = q . i by A2, Th14;
hence Sum (mlt (p,q)) = q . i by A5, A3, Th12; :: thesis: verum