let K be Ring; :: 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 holds
( ( 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 ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . 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 holds
( ( 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 ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . 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 holds
( ( 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 ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . 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 holds
( ( 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 ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . 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 ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . j = 0. K ) ) ) )
thus ( 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 ) ) ) :: thesis: ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . j = 0. K ) ) )

proof

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 Th13, 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 = (1. K) * b by A1, A3, FVSUM_1:60
.= q . i by A7 ;
:: 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 ;
:: thesis: verum

end;

thus ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . j = 0. K ) ) ) :: thesis: verum

proof

assume A9: j in dom (mlt (q,p)) ; :: thesis: ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . j = 0. K ) )
A10: ( 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 (q,p)) = Seg (len (mlt (q,p))) & len (mlt (q,p)) = min ((len q),(len p)) ) by Th13, FINSEQ_1:def 3;
then A11: j in (dom q) /\ (dom p) by A9, A10, FINSEQ_2:2;
then A12: 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 (q,p)) . j = q . i ) :: thesis: ( i <> j implies (mlt (q,p)) . j = 0. K )

proof

reconsider b = q . j1 as Element of K by A12, FINSEQ_2:11;
assume A13: i = j ; :: thesis: (mlt (q,p)) . j = q . i
hence (mlt (q,p)) . j = b * (1. K) by A1, A9, FVSUM_1:60
.= q . i by A13 ;
:: thesis: verum

end;

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

end;