let k be Nat; :: thesis: for p, q being FinSequence of REAL st len p = len q & p has_onlyone_value_in k holds
( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) )
let p, q be FinSequence of REAL ; :: thesis: ( len p = len q & p has_onlyone_value_in k implies ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) ) )
assume that
A1: len p = len q and
A2: p has_onlyone_value_in k ; :: thesis: ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) )
len (mlt (p,q)) = len p by A1, MATRPROB:30;
then A3: dom (mlt (p,q)) = dom p by FINSEQ_3:29;

A4: now :: thesis: for i being Nat st i in dom (mlt (p,q)) & i <> k holds
(mlt (p,q)) . i = 0

let i be Nat; :: thesis: ( i in dom (mlt (p,q)) & i <> k implies (mlt (p,q)) . i = 0 )
assume that
A5: i in dom (mlt (p,q)) and
A6: i <> k ; :: thesis: (mlt (p,q)) . i = 0
thus (mlt (p,q)) . i = (p . i) * (q . i) by RVSUM_1:59
.= 0 * (q . i) by A2, A3, A5, A6
.= 0 ; :: thesis: verum

end;

k in dom (mlt (p,q)) by A2, A3;
hence ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) ) by A4, RVSUM_1:59; :: thesis: verum