let k be Element of 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:31;

A4: now

let i be Element of 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 A5, RVSUM_1:86
.= 0 * (q . i) by A2, A3, A5, A6, Def2
.= 0 ; :: thesis: verum

end;

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